theorem Th35: :: REWRITE1:35

for R being Relation
for a being object st not a in field R holds
a is_a_normal_form_of a,R by Th12, Th34;