let X be set ; :: thesis: 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) )
let EqR be Equivalence_Relation of X; :: thesis: 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) )
let x, y be object ; :: thesis: ( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
A1: ( not [x,y] in EqR implies Class (EqR,x) misses Class (EqR,y) )

proof

assume A2: not [x,y] in EqR ; :: thesis: Class (EqR,x) misses Class (EqR,y)
assume Class (EqR,x) meets Class (EqR,y) ; :: thesis: contradiction
then consider z being object such that
A3: z in Class (EqR,x) and
A4: z in Class (EqR,y) by XBOOLE_0:3;
[z,x] in EqR by A3, Th19;
then A5: [x,z] in EqR by Th6;
[z,y] in EqR by A4, Th19;
hence contradiction by A2, A5, Th7; :: thesis: verum

end;

assume A6: y in X ; :: thesis: ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) )

proof

assume [x,y] in EqR ; :: thesis: Class (EqR,x) = Class (EqR,y)
then x in Class (EqR,y) by Th19;
hence Class (EqR,x) = Class (EqR,y) by A6, Th23; :: thesis: verum

end;

hence ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) ) by A1; :: thesis: verum