let A be set ; :: thesis: for R being Relation of A
for E being Equivalence_Relation of A st R c= E holds
for a, b being set st a in A & b in A & a,b are_convertible_wrt R holds
[a,b] in E
let R be Relation of A; :: thesis: for E being Equivalence_Relation of A st R c= E holds
for a, b being set st a in A & b in A & a,b are_convertible_wrt R holds
[a,b] in E
let E be Equivalence_Relation of A; :: thesis: ( R c= E implies for a, b being set st a in A & b in A & a,b are_convertible_wrt R holds
[a,b] in E )
assume A1: R c= E ; :: thesis: for a, b being set st a in A & b in A & a,b are_convertible_wrt R holds
[a,b] in E
let a, b be set ; :: thesis: ( a in A & b in A & a,b are_convertible_wrt R implies [a,b] in E )
assume A2: ( a in A & b in A ) ; :: thesis: ( not a,b are_convertible_wrt R or [a,b] in E )
assume R \/ (R ~ ) reduces a,b ; :: according to REWRITE1:def 4 :: thesis: [a,b] in E
then consider p being RedSequence of R \/ (R ~ ) such that
A3: ( p . 1 = a & p . (len p) = b ) by REWRITE1:def 3;
defpred S₁[ Element of NAT ] means ( $1 in dom p implies [a,(p . $1)] in E );
A4: S₁[ 0 ] by FINSEQ_3:27;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume that
A6: ( i in dom p implies [a,(p . i)] in E ) and
A7: i + 1 in dom p ; :: thesis: [a,(p . (i + 1))] in E
( i <= i + 1 & i + 1 <= len p ) by A7, FINSEQ_3:27, NAT_1:11;
then A8: i <= len p by XXREAL_0:2;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: [a,(p . (i + 1))] in E

hence [a,(p . (i + 1))] in E by A2, A3, EQREL_1:11; :: thesis: verum

end;

suppose i > 0 ; :: thesis: [a,(p . (i + 1))] in E

then A9: i >= 0 + 1 by NAT_1:13;
then i in dom p by A8, FINSEQ_3:27;
then A10: [(p . i),(p . (i + 1))] in R \/ (R ~ ) by A7, REWRITE1:def 2;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in R ~ ) by XBOOLE_0:def 3;
then A11: ( [(p . i),(p . (i + 1))] in R or [(p . (i + 1)),(p . i)] in R ) by RELAT_1:def 7;
reconsider ppi = p . i, pj = p . (i + 1) as Element of A by A10, ZFMISC_1:106;
( [ppi,pj] in E & [a,ppi] in E ) by A1, A6, A8, A9, A11, EQREL_1:12, FINSEQ_3:27;
hence [a,(p . (i + 1))] in E by EQREL_1:13; :: thesis: verum

end;

end;

end;

A12: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A4, A5);
len p in dom p by FINSEQ_5:6;
hence [a,b] in E by A3, A12; :: thesis: verum