theorem Th4: :: LATTICE5:4

for A, x being set holds
( x in the carrier of (EqRelLATT A) iff x is Equivalence_Relation of A )