let X be set ; :: thesis: for EqR being Equivalence_Relation of X
for x, y being set 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 set holds
( not y in X or Class EqR,x = Class EqR,y or Class EqR,x misses Class EqR,y )
let x, y be set ; :: 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 set 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, Th27;
then A5: [x,z] in EqR by Th12;
[z,y] in EqR by A4, Th27;
hence contradiction by A2, A5, Th13; :: 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 Th27;
hence Class EqR,x = Class EqR,y by A6, Th31; :: thesis: verum

end;

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