let R be Relation; :: thesis: ( R is subcommutative implies for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
assume A1: R is subcommutative ; :: thesis: for a, b, c being set st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
let a, b, c be set ; :: thesis: ( R reduces a,b & [a,c] in R implies b,c are_convergent_wrt R )
given p being RedSequence of R such that A2: ( p . 1 = a & p . (len p) = b ) ; :: according to REWRITE1:def 3 :: thesis: ( not [a,c] in R or b,c are_convergent_wrt R )
A3: len p in dom p by FINSEQ_5:6;
assume A4: [a,c] in R ; :: thesis: b,c are_convergent_wrt R
defpred S₁[ Element of NAT ] means ( $1 in dom p implies ex d being set st
( ( [(p . $1),d] in R or p . $1 = d ) & R reduces c,d ) );
A5: S₁[ 0 ] by Lm1;

now

let i be Element of NAT ; :: thesis: ( ( i in dom p implies S₁[i] ) & i + 1 in dom p implies S₁[b₁ + 1] )
assume that
A6: ( i in dom p implies S₁[i] ) and
A7: i + 1 in dom p ; :: thesis: S₁[b₁ + 1]

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

suppose i = 0 ; :: thesis: S₁[b₁ + 1]

then ( p . (i + 1) = a & R reduces c,c ) by A2, Th13;
hence S₁[i + 1] by A4; :: thesis: verum

end;

suppose i > 0 ; :: thesis: S₁[b₁ + 1]

then A8: ( i >= 0 + 1 & i < len p ) by A7, Lm2, NAT_1:13;
then A9: i in dom p by Lm3;
consider d being set such that
A10: ( ( [(p . i),d] in R or p . i = d ) & R reduces c,d ) by A6, A8, Lm3;
A11: [(p . i),(p . (i + 1))] in R by A7, A9, Def2;

A12: now

assume [(p . i),d] in R ; :: thesis: ex e being set st
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )
then p . (i + 1),d are_convergent<=1_wrt R by A1, A11, Def21;
then consider e being set such that
A13: ( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & ( [d,e] in R or d = e ) ) by Def9;
take e = e; :: thesis: ( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )
thus ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) by A13; :: thesis: R reduces c,e
R reduces d,e by A13, Th13, Th16;
hence R reduces c,e by A10, Th17; :: thesis: verum

end;

now

assume p . i = d ; :: thesis: R reduces c,p . (i + 1)
then R reduces d,p . (i + 1) by A11, Th16;
hence R reduces c,p . (i + 1) by A10, Th17; :: thesis: verum

end;

hence S₁[i + 1] by A10, A12; :: thesis: verum

end;

end;

end;

then A14: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A5, A14);
then consider d being set such that
A15: ( ( [b,d] in R or b = d ) & R reduces c,d ) by A2, A3;
take d ; :: according to REWRITE1:def 7 :: thesis: ( R reduces b,d & R reduces c,d )
thus ( R reduces b,d & R reduces c,d ) by A15, Th13, Th16; :: thesis: verum