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

( y in Class (EqR,x) 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

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

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

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

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

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

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

then [x,y] in EqR by A1, Lm2;

then [y,x] in EqR by Th6;

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

for EqR being Equivalence_Relation of X

for x being object st x in X holds

( y in Class (EqR,x) 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

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

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

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

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

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

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

proof

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

then [y,x] in EqR by Th19;

then [x,y] in EqR by Th6;

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

end;then [y,x] in EqR by Th19;

then [x,y] in EqR by Th6;

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

then [x,y] in EqR by A1, Lm2;

then [y,x] in EqR by Th6;

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