:: deftheorem Def14 defines weakly-normalizing REWRITE1:def 14 :
for R being Relation holds
( R is weakly-normalizing iff for a being object st a in field R holds
a has_a_normal_form_wrt R );