rwa [setOf_rel_eq ht hp]
case intro.intro.intro
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t✝ : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
hx : x ∈ s
t : Set α
ht : t ∈ P
hp : x ∈ t
⊢ {y | P.Rel x y} ∈ P
no goals