:: deftheorem Def13 defines -class FOMODEL3:def 13 :
for X being non empty set
for E being Equivalence_Relation of X
for b₃ being Function of X,(Class E) holds
( b₃ = E -class iff for x being Element of X holds b₃ . x = EqClass (E,x) );