:: deftheorem defines are_divergent_wrt REWRITE1:def 8 :
for R being Relation
for a, b being object holds
( a,b are_divergent_wrt R iff ex c being object st
( R reduces c,a & R reduces c,b ) );