defpred S₁[ set ] means $1 in X;
A1: S₁[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 & S₁[y] holds
S₁[z]

proof

let y, z be set ; :: thesis: ( R reduces x,y & [y,z] in R & S₁[y] implies S₁[z] )
assume R reduces x,y ; :: thesis: ( not [y,z] in R or not S₁[y] or S₁[z] )
assume A4: [y,z] in R ; :: thesis: ( not S₁[y] or S₁[z] )
( z in field R & field R c= X \/ X ) by A4, RELAT_1:15, RELSET_1:8;
hence ( not S₁[y] or S₁[z] ) ; :: thesis: verum

end;

S₁[ nf (x,R)] from MSAFREE4:sch 5(A1, A2, A3);
hence nf (x,R) is Element of X ; :: thesis: verum