theorem Th34: :: REWRITE1:34

for R being Relation
for a being object st not a in field R holds
a is_a_normal_form_wrt R by RELAT_1:15;