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 S1[ object , object ] means $1,$2 are_convertible_wrt R;
consider Q being Relation of A such that
A1: for a, b being object holds
( [a,b] in Q iff ( a in A & b in A & S1[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: now :: thesis: for E being Equivalence_Relation of A st R c= E holds
Q c= E
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 object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in Q or [x,y] in E )
assume A4: [x,y] in Q ; :: thesis: [x,y] in E
then A5: x,y are_convertible_wrt R by A1;
x in A by A1, A4;
hence [x,y] in E by A3, A5, Th40; :: thesis: verum
end;
end;
R c= Q
proof
let a, b be object ; :: according to RELAT_1:def 3 :: thesis: ( not [a,b] in R or [a,b] in Q )
assume A6: [a,b] in R ; :: thesis: [a,b] in Q
then A7: b in A by ZFMISC_1:87;
A8: a,b are_convertible_wrt R by A6, REWRITE1:29;
a in A by A6, ZFMISC_1:87;
hence [a,b] in Q by A1, A7, A8; :: thesis: verum
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