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