theorem Th36: :: REWRITE1:36

for R being 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 )