let R, Q be Relation; :: thesis: ( ( for a, b being object st [a,b] in Q holds
a,b are_critical_wrt R ) implies R,R \/ Q are_equivalent )
assume A1: for a, b being object st [a,b] in Q holds
a,b are_critical_wrt R ; :: thesis: R,R \/ Q are_equivalent
let a, b be object ; :: according to REWRITE1:def 26 :: thesis: ( a,b are_convertible_wrt R iff a,b are_convertible_wrt R \/ Q )
A2: R c= R \/ Q by XBOOLE_1:7;
A3: R ~ c= (R \/ Q) ~

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R ~ or [x,y] in (R \/ Q) ~ )
assume [x,y] in R ~ ; :: thesis: [x,y] in (R \/ Q) ~
then [y,x] in R by RELAT_1:def 7;
hence [x,y] in (R \/ Q) ~ by A2, RELAT_1:def 7; :: thesis: verum

end;

thus ( a,b are_convertible_wrt R implies a,b are_convertible_wrt R \/ Q ) by A2, A3, Th22, XBOOLE_1:13; :: thesis: ( a,b are_convertible_wrt R \/ Q implies a,b are_convertible_wrt R )
given p being RedSequence of (R \/ Q) \/ ((R \/ Q) ~) such that A4: a = p . 1 and
A5: b = p . (len p) ; :: according to REWRITE1:def 3,REWRITE1:def 4 :: thesis: a,b are_convertible_wrt R
defpred S₁[ Nat] means ( $1 in dom p implies a,p . $1 are_convertible_wrt R );

now :: thesis: for i being Nat st ( i in dom p implies a,p . i are_convertible_wrt R ) & i + 1 in dom p holds
a,p . (i + 1) are_convertible_wrt R

let i be Nat; :: thesis: ( ( i in dom p implies a,p . i are_convertible_wrt R ) & i + 1 in dom p implies a,p . (b₁ + 1) are_convertible_wrt R )
assume that
A6: ( i in dom p implies a,p . i are_convertible_wrt R ) and
A7: i + 1 in dom p ; :: thesis: a,p . (b₁ + 1) are_convertible_wrt R
A8: i < len p by A7, Lm2;

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

suppose i = 0 ; :: thesis: a,p . (b₁ + 1) are_convertible_wrt R

hence a,p . (i + 1) are_convertible_wrt R by A4, Th26; :: thesis: verum

end;

suppose A9: i > 0 ; :: thesis: a,p . (b₁ + 1) are_convertible_wrt R

then i in dom p by A8, Lm3;
then [(p . i),(p . (i + 1))] in (R \/ Q) \/ ((R \/ Q) ~) by A7, Def2;
then ( [(p . i),(p . (i + 1))] in R \/ Q or [(p . i),(p . (i + 1))] in (R \/ Q) ~ ) by XBOOLE_0:def 3;
then ( [(p . i),(p . (i + 1))] in R \/ Q or [(p . (i + 1)),(p . i)] in R \/ Q ) by RELAT_1:def 7;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in Q or [(p . (i + 1)),(p . i)] in R or [(p . (i + 1)),(p . i)] in Q ) by XBOOLE_0:def 3;
then ( p . i,p . (i + 1) are_convertible_wrt R or p . (i + 1),p . i are_convertible_wrt R ) by A1, Th29, Th59;
then p . i,p . (i + 1) are_convertible_wrt R by Lm5;
hence a,p . (i + 1) are_convertible_wrt R by A6, A8, A9, Lm3, Th30; :: thesis: verum

end;

end;

end;

then A10: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A11: len p in dom p by FINSEQ_5:6;
A12: S₁[ 0 ] by Lm1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A12, A10);
hence a,b are_convertible_wrt R by A5, A11; :: thesis: verum