let R be Relation; :: thesis: for a, b, c being set 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 set ; :: 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 set such that
A3: R reduces d,b and
A4: R reduces d,c by Def8;
R reduces d,a by A2, A3, Th17;
hence a,c are_divergent_wrt R by A4, Def8; :: 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 set such that
A6: R reduces d,a and
A7: R reduces d,b by Def8;
R reduces d,c by A5, A7, Th17;
hence a,c are_divergent_wrt R by A6, Def8; :: thesis: verum

end;

end;