defpred S1[ set ] means $1 in X;
A1: S1[x] ;
 nf (x,R) is_a_normal_form_of x,R by REWRITE1:54;
then A2: R reduces x, nf (x,R) ;
A3: for y, z being set st R reduces x,y & [y,z] in R & S1[y] holds
S1[z]
proof
let y, z be set ; :: thesis: ( R reduces x,y & [y,z] in R & S1[y] implies S1[z] )
assume R reduces x,y ; :: thesis: ( not [y,z] in R or not S1[y] or S1[z] )
assume A4: [y,z] in R ; :: thesis: ( not S1[y] or S1[z] )
( z in field R & field R c= X \/ X ) by A4, RELAT_1:15, RELSET_1:8;
hence ( not S1[y] or S1[z] ) ; :: thesis: verum
end;
S1[ nf (x,R)] from MSAFREE4:sch 5(A1, A2, A3);
 hence nf (x,R) is Element of X ; :: thesis: verum