let R be Relation; :: thesis: for a, b, c being set 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 set ; :: 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 set such that
A3: ( R reduces b,d & R reduces c,d ) by Def7;
R reduces a,d by A2, A3, Th17;
hence a,c are_convergent_wrt R by A3, Def7; :: thesis: verum

end;

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

then consider d being set such that
A5: ( R reduces a,d & R reduces b,d ) by Def7;
R reduces c,d by A4, A5, Th17;
hence a,c are_convergent_wrt R by A5, Def7; :: thesis: verum

end;

end;