:: deftheorem defines is_a_normal_form_of REWRITE1:def 6 :
for R being Relation
for a, b being object holds
( b is_a_normal_form_of a,R iff ( b is_a_normal_form_wrt R & R reduces a,b ) );