let R be Relation; :: thesis: for a, b, c being object st ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) holds
a,c are_convergent_wrt R
let a, b, c be object ; :: thesis: ( ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) implies a,c are_convergent_wrt R )
assume A1: ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) ; :: thesis: a,c are_convergent_wrt R

per cases ( ( R reduces a,b & b,c are_convergent_wrt R ) or ( a,b are_convergent_wrt R & R reduces c,b ) ) by A1;

suppose A2: ( R reduces a,b & b,c are_convergent_wrt R ) ; :: thesis: a,c are_convergent_wrt R

then consider d being object such that
A3: R reduces b,d and
A4: R reduces c,d ;
R reduces a,d by A2, A3, Th16;
hence a,c are_convergent_wrt R by A4; :: thesis: verum

end;

suppose A5: ( a,b are_convergent_wrt R & R reduces c,b ) ; :: thesis: a,c are_convergent_wrt R

then consider d being object such that
A6: R reduces a,d and
A7: R reduces b,d ;
R reduces c,d by A5, A7, Th16;
hence a,c are_convergent_wrt R by A6; :: thesis: verum

end;

end;