:: deftheorem defines has_a_normal_form_wrt REWRITE1:def 11 :
for R being Relation
for a being object holds
( a has_a_normal_form_wrt R iff ex b being object st b is_a_normal_form_of a,R );