:: deftheorem defines with_NF_property REWRITE1:def 20 :
for R being Relation holds
( R is with_NF_property iff for a, b being object st a is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
R reduces b,a );