:: deftheorem defines Intersection EQREL_1:def 8 :
for X being non empty set
for F being non empty Part-Family of X
for b₃ being non empty a_partition of X holds
( b₃ = Intersection F iff for x being Element of X holds EqClass (x,b₃) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } );