:: deftheorem Def23 defines with_Church-Rosser_property REWRITE1:def 23 :
for R being Relation holds
( R is with_Church-Rosser_property iff for a, b being object st a,b are_convertible_wrt R holds
a,b are_convergent_wrt R );