theorem Th24: :: EQREL_1:24

for X being set
for EqR being Equivalence_Relation of X
for x, y being object holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )