let X be ARS ; :: thesis: for x being Element of X holds
( x is normform iff x is_a_normal_form_wrt the reduction of X )
let x be Element of X; :: thesis: ( x is normform iff x is_a_normal_form_wrt the reduction of X )
set R = the reduction of X;
thus ( x is normform implies x is_a_normal_form_wrt the reduction of X ) :: thesis: ( x is_a_normal_form_wrt the reduction of X implies x is normform )

proof

assume Z0: for y being Element of X holds not x ==> y ; :: according to ABSRED_0:def 11 :: thesis: x is_a_normal_form_wrt the reduction of X
let a be object ; :: according to REWRITE1:def 5 :: thesis: not [x,a] in the reduction of X
assume Z1: [x,a] in the reduction of X ; :: thesis: contradiction
then reconsider y = a as Element of X by ZFMISC_1:87;
x ==> y by Z1;
hence contradiction by Z0; :: thesis: verum

end;

assume Z1: for b being object holds not [x,b] in the reduction of X ; :: according to REWRITE1:def 5 :: thesis: x is normform
let y be Element of X; :: according to ABSRED_0:def 11 :: thesis: not x ==> y
assume [x,y] in the reduction of X ; :: according to ABSRED_0:def 1 :: thesis: contradiction
hence contradiction by Z1; :: thesis: verum