:: deftheorem defines are_convertible_wrt REWRITE1:def 4 :
for R being Relation
for a, b being object holds
( a,b are_convertible_wrt R iff R \/ (R ~) reduces a,b );