let X be ARS ; :: thesis: for x being Element of X holds
( x is normalizable iff x has_a_normal_form_wrt the reduction of X )
let x be Element of X; :: thesis: ( x is normalizable iff x has_a_normal_form_wrt the reduction of X )
set R = the reduction of X;
A0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
thus ( x is normalizable implies x has_a_normal_form_wrt the reduction of X ) :: thesis: ( x has_a_normal_form_wrt the reduction of X implies x is normalizable )

proof

given y being Element of X such that A1: y is_normform_of x ; :: according to ABSRED_0:def 13 :: thesis: x has_a_normal_form_wrt the reduction of X
take y ; :: according to REWRITE1:def 11 :: thesis: y is_a_normal_form_of x, the reduction of X
thus y is_a_normal_form_of x, the reduction of X by A1, Ch2; :: thesis: verum

end;

given a being object such that A2: a is_a_normal_form_of x, the reduction of X ; :: according to REWRITE1:def 11 :: thesis: x is normalizable
the reduction of X reduces x,a by A2, REWRITE1:def 6;
then ( x = a or a in field the reduction of X ) by REWRITE1:18;
then reconsider a = a as Element of X by A0;
take a ; :: according to ABSRED_0:def 13 :: thesis: a is_normform_of x
thus a is_normform_of x by A2, Ch2; :: thesis: verum