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 and
A3: p . (len p) = b ; :: according to REWRITE1:def 3 :: thesis: ( not [a,c] in R or 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 ) );
assume A4: [a,c] in R ; :: thesis: b,c are_convergent_wrt R

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
A5: ( i in dom p implies S₁[i] ) and
A6: i + 1 in dom p ; :: thesis: S₁[b₁ + 1]

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

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

R reduces c,c by Th13;
hence S₁[i + 1] by A2, A4, A7; :: thesis: verum

end;

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

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

A13: 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, A12, Def21;
then consider e being set such that
A14: ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) and
A15: ( [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 A14; :: thesis: R reduces c,e
R reduces d,e by A15, Th13, Th16;
hence R reduces c,e by A11, Th17; :: thesis: verum

end;

now

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

end;

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

end;

end;

end;

then A16: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A17: len p in dom p by FINSEQ_5:6;
A18: S₁[ 0 ] by Lm1;
for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A18, A16);
then consider d being set such that
A19: ( ( [b,d] in R or b = d ) & R reduces c,d ) by A3, A17;
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 A19, Th13, Th16; :: thesis: verum