let R be Relation; :: thesis: for a, b being set st R reduces a,b holds
( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R )
let a, b be set ; :: thesis: ( R reduces a,b implies ( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R ) )
( R reduces a,a & R reduces b,b ) by Th13;
hence ( R reduces a,b implies ( a,b are_convergent_wrt R & a,b are_divergent_wrt R & b,a are_convergent_wrt R & b,a are_divergent_wrt R ) ) by Def7, Def8; :: thesis: verum