:: deftheorem defines are_equivalent REWRITE1:def 26 :
for R, Q being Relation holds
( R,Q are_equivalent iff for a, b being object holds
( a,b are_convertible_wrt R iff a,b are_convertible_wrt Q ) );