theorem Th39: :: REWRITE1:39

for a, b being object st ( a,b are_convergent_wrt {} or a,b are_divergent_wrt {} ) holds
a = b