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:
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 ; :: 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 ;
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:
thus a is_normform_of x by ; :: thesis: verum