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) )

( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) )

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 A6:
y in X
; :: thesis: ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
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 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

( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) )

proof

hence
( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
by A1; :: thesis: verum
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;then x in Class (EqR,y) by Th19;

hence Class (EqR,x) = Class (EqR,y) by A6, Th23; :: thesis: verum