no goals
ι : Sort ?u.9595
α : Type u_2
β : Type u_1
γ : Type ?u.9604
κ : ι → Sort ?u.9609
r : α → β → Prop
s s₁ s₂ : Set α
t t₁ t₂ : Set β
c d : Concept α β r
⊢ c.snd ⊂ d.snd ↔ d < c
rw [ssubset_iff_subset_not_subset, lt_iff_le_not_le, snd_subset_snd_iff, snd_subset_snd_iff]