let R be Relation; 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 ; ( 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 ) )
; verum