theorem Th46: :: REWRITE1:46

for R being Relation
for a being object st not a in field R holds
a has_a_normal_form_wrt R by Th35;