let X be ARS ; :: thesis: for x, y being Element of X holds
( x is_normform_of y iff x is_a_normal_form_of y, the reduction of X )
let x, y be Element of X; :: thesis: ( x is_normform_of y iff x is_a_normal_form_of y, the reduction of X )
set R = the reduction of X;
thus ( x is_normform_of y implies x is_a_normal_form_of y, the reduction of X ) :: thesis: ( x is_a_normal_form_of y, the reduction of X implies x is_normform_of y )

proof

assume ( x is normform & the reduction of X reduces y,x ) ; :: according to ABSRED_0:def 3,ABSRED_0:def 12 :: thesis: x is_a_normal_form_of y, the reduction of X
hence ( x is_a_normal_form_wrt the reduction of X & the reduction of X reduces y,x ) by Ch1; :: according to REWRITE1:def 6 :: thesis: verum

end;

assume ( x is_a_normal_form_wrt the reduction of X & the reduction of X reduces y,x ) ; :: according to REWRITE1:def 6 :: thesis: x is_normform_of y
hence ( x is normform & the reduction of X reduces y,x ) by Ch1; :: according to ABSRED_0:def 3,ABSRED_0:def 12 :: thesis: verum