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

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

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

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

end;

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

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

end;

end;