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