let R be Relation; :: thesis: for a being set st not a in field R holds
a has_a_normal_form_wrt R
let a be set ; :: thesis: ( not a in field R implies a has_a_normal_form_wrt R )
assume not a in field R ; :: thesis: a has_a_normal_form_wrt R
hence ex b being set st b is_a_normal_form_of a,R by Th36; :: according to REWRITE1:def 11 :: thesis: verum