:: deftheorem Def19 defines with_UN_property REWRITE1:def 19 :
for R being Relation holds
( R is with_UN_property iff for a, b being object st a is_a_normal_form_wrt R & b is_a_normal_form_wrt R & a,b are_convertible_wrt R holds
a = b );