let X be set ; :: thesis: for y being object

for EqR being Equivalence_Relation of X

for x being object st x in X holds

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

let y be object ; :: thesis: for EqR being Equivalence_Relation of X

for x being object st x in X holds

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

let EqR be Equivalence_Relation of X; :: thesis: for x being object st x in X holds

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

let x be object ; :: thesis: ( x in X implies ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) )

assume A1: x in X ; :: thesis: ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )

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

then x in Class (EqR,y) by A1, Th20;

hence [x,y] in EqR by Th19; :: thesis: verum

for EqR being Equivalence_Relation of X

for x being object st x in X holds

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

let y be object ; :: thesis: for EqR being Equivalence_Relation of X

for x being object st x in X holds

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

let EqR be Equivalence_Relation of X; :: thesis: for x being object st x in X holds

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

let x be object ; :: thesis: ( x in X implies ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) )

assume A1: x in X ; :: thesis: ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )

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

proof

assume
Class (EqR,x) = Class (EqR,y)
; :: thesis: [x,y] in EqR
assume A2:
[x,y] in EqR
; :: thesis: Class (EqR,x) = Class (EqR,y)

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

end;now :: thesis: for z being object st z in Class (EqR,y) holds

z in Class (EqR,x)

then A4:
Class (EqR,y) c= Class (EqR,x)
;z in Class (EqR,x)

let z be object ; :: thesis: ( z in Class (EqR,y) implies z in Class (EqR,x) )

assume z in Class (EqR,y) ; :: thesis: z in Class (EqR,x)

then A3: [z,y] in EqR by Th19;

[y,x] in EqR by A2, Th6;

then [z,x] in EqR by A3, Th7;

hence z in Class (EqR,x) by Th19; :: thesis: verum

end;assume z in Class (EqR,y) ; :: thesis: z in Class (EqR,x)

then A3: [z,y] in EqR by Th19;

[y,x] in EqR by A2, Th6;

then [z,x] in EqR by A3, Th7;

hence z in Class (EqR,x) by Th19; :: thesis: verum

now :: thesis: for z being object st z in Class (EqR,x) holds

z in Class (EqR,y)

then
Class (EqR,x) c= Class (EqR,y)
;z in Class (EqR,y)

let z be object ; :: thesis: ( z in Class (EqR,x) implies z in Class (EqR,y) )

assume z in Class (EqR,x) ; :: thesis: z in Class (EqR,y)

then [z,x] in EqR by Th19;

then [z,y] in EqR by A2, Th7;

hence z in Class (EqR,y) by Th19; :: thesis: verum

end;assume z in Class (EqR,x) ; :: thesis: z in Class (EqR,y)

then [z,x] in EqR by Th19;

then [z,y] in EqR by A2, Th7;

hence z in Class (EqR,y) by Th19; :: thesis: verum

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

then x in Class (EqR,y) by A1, Th20;

hence [x,y] in EqR by Th19; :: thesis: verum