let A be set ; for R being Relation of A
for E being Equivalence_Relation of A st R c= E holds
for a, b being object st a in A & a,b are_convertible_wrt R holds
[a,b] in E
let R be Relation of A; for E being Equivalence_Relation of A st R c= E holds
for a, b being object st a in A & a,b are_convertible_wrt R holds
[a,b] in E
let E be Equivalence_Relation of A; ( R c= E implies for a, b being object st a in A & a,b are_convertible_wrt R holds
[a,b] in E )
assume A1:
R c= E
; for a, b being object st a in A & a,b are_convertible_wrt R holds
[a,b] in E
let a, b be object ; ( a in A & a,b are_convertible_wrt R implies [a,b] in E )
assume A2:
a in A
; ( not a,b are_convertible_wrt R or [a,b] in E )
assume
R \/ (R ~) reduces a,b
; REWRITE1:def 4 [a,b] in E
then consider p being RedSequence of R \/ (R ~) such that
A3:
p . 1 = a
and
A4:
p . (len p) = b
;
defpred S1[ Nat] means ( $1 in dom p implies [a,(p . $1)] in E );
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume that A6:
(
i in dom p implies
[a,(p . i)] in E )
and A7:
i + 1
in dom p
;
[a,(p . (i + 1))] in E
A8:
i <= i + 1
by NAT_1:11;
i + 1
<= len p
by A7, FINSEQ_3:25;
then A9:
i <= len p
by A8, XXREAL_0:2;
per cases
( i = 0 or i > 0 )
;
suppose
i > 0
;
[a,(p . (i + 1))] in Ethen A10:
i >= 0 + 1
by NAT_1:13;
then
i in dom p
by A9, FINSEQ_3:25;
then A11:
[(p . i),(p . (i + 1))] in R \/ (R ~)
by A7, REWRITE1:def 2;
then reconsider ppi =
p . i,
pj =
p . (i + 1) as
Element of
A by ZFMISC_1:87;
(
[(p . i),(p . (i + 1))] in R or
[(p . i),(p . (i + 1))] in R ~ )
by A11, XBOOLE_0:def 3;
then
(
[(p . i),(p . (i + 1))] in R or
[(p . (i + 1)),(p . i)] in R )
by RELAT_1:def 7;
then
[ppi,pj] in E
by A1, EQREL_1:6;
hence
[a,(p . (i + 1))] in E
by A6, A9, A10, EQREL_1:7, FINSEQ_3:25;
verum end; end;
end;
A12:
len p in dom p
by FINSEQ_5:6;
A13:
S1[ 0 ]
by FINSEQ_3:25;
for i being Nat holds S1[i]
from NAT_1:sch 2(A13, A5);
hence
[a,b] in E
by A4, A12; verum