let R be Relation; :: thesis: for a being set st not a in field R holds
a is_a_normal_form_of a,R
let a be set ; :: thesis: ( not a in field R implies a is_a_normal_form_of a,R )
assume not a in field R ; :: thesis: a is_a_normal_form_of a,R
hence ( a is_a_normal_form_wrt R & R reduces a,a ) by Th13, Th35; :: according to REWRITE1:def 6 :: thesis: verum