theorem Th38: :: REWRITE1:38

for R being Relation
for a being object holds
( a,a are_convergent_wrt R & a,a are_divergent_wrt R ) by Th12;