:: deftheorem defines are_divergent<=1_wrt REWRITE1:def 10 :
for R being Relation
for a, b being object holds
( a,b are_divergent<=1_wrt R iff ex c being object st
( ( [c,a] in R or a = c ) & ( [c,b] in R or b = c ) ) );