:: deftheorem defines is_a_normal_form_wrt REWRITE1:def 5 :
for R being Relation
for a being object holds
( a is_a_normal_form_wrt R iff for b being object holds not [a,b] in R );