let R be Relation; :: thesis: for a, b being object 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 object ; :: 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 Th12;
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 ) ) ; :: thesis: verum