let R be Relation; :: thesis: for a being set st not a in field R holds
a is_a_normal_form_wrt R
let a be set ; :: thesis: ( not a in field R implies a is_a_normal_form_wrt R )
assume A1: not a in field R ; :: thesis: a is_a_normal_form_wrt R
assume ex b being set st [a,b] in R ; :: according to REWRITE1:def 5 :: thesis: contradiction
hence contradiction by A1, RELAT_1:15; :: thesis: verum