let A be non empty set ; :: thesis: for R being Relation of A
for a, b being Element of A holds
( [a,b] in EqCl R iff a,b are_convertible_wrt R )
let R be Relation of A; :: thesis: for a, b being Element of A holds
( [a,b] in EqCl R iff a,b are_convertible_wrt R )
defpred S₁[ set , set ] means $1,$2 are_convertible_wrt R;
consider Q being Relation of A such that
A1: for a, b being set holds
( [a,b] in Q iff ( a in A & b in A & S₁[a,b] ) ) from RELSET_1:sch 1();
for a, b being set st a in A & b in A holds
( [a,b] in Q iff a,b are_convertible_wrt R ) by A1;
then reconsider Q = Q as Equivalence_Relation of A by Th39;
A2: R c= Q

proof

let a, b be set ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in R or [a,b] in Q )
assume [a,b] in R ; :: thesis: [a,b] in Q
then ( a in A & b in A & a,b are_convertible_wrt R ) by REWRITE1:30, ZFMISC_1:106;
hence [a,b] in Q by A1; :: thesis: verum

end;

now

let E be Equivalence_Relation of A; :: thesis: ( R c= E implies Q c= E )
assume A3: R c= E ; :: thesis: Q c= E
thus Q c= E :: thesis: verum

proof

let x, y be set ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in Q or [x,y] in E )
assume [x,y] in Q ; :: thesis: [x,y] in E
then ( x in A & y in A & x,y are_convertible_wrt R ) by A1;
hence [x,y] in E by A3, Th40; :: thesis: verum

end;

end;

then Q = EqCl R by A2, MSUALG_5:def 1;
hence for a, b being Element of A holds
( [a,b] in EqCl R iff a,b are_convertible_wrt R ) by A1; :: thesis: verum