let X be ARS ; :: thesis: ( X is N.F. iff the reduction of X is with_NF_property )
set R = the reduction of X;
set A = the carrier of X;
A0: field the reduction of X c= the carrier of X \/ the carrier of X by RELSET_1:8;
thus ( X is N.F. implies the reduction of X is with_NF_property ) :: thesis: ( the reduction of X is with_NF_property implies X is N.F. )

proof

assume A1: for x, y being Element of X st x is normform & x <=*=> y holds
y =*=> x ; :: according to ABSRED_0:def 18 :: thesis: the reduction of X is with_NF_property
let a, b be object ; :: according to REWRITE1:def 20 :: thesis: ( not a is_a_normal_form_wrt the reduction of X or not a,b are_convertible_wrt the reduction of X or the reduction of X reduces b,a )
assume A2: ( a is_a_normal_form_wrt the reduction of X & a,b are_convertible_wrt the reduction of X ) ; :: thesis: the reduction of X reduces b,a

per cases ( ( a in the carrier of X & b in the carrier of X ) or not a in the carrier of X or not b in the carrier of X ) ;

suppose ( a in the carrier of X & b in the carrier of X ) ; :: thesis: the reduction of X reduces b,a

then reconsider x = a, y = b as Element of X ;
( x is normform & x <=*=> y ) by A2, Ch1;
then y =*=> x by A1;
hence the reduction of X reduces b,a ; :: thesis: verum

end;

suppose ( not a in the carrier of X or not b in the carrier of X ) ; :: thesis: the reduction of X reduces b,a

then ( not a in field the reduction of X or not b in field the reduction of X ) by A0;
then a = b by A2, REWRITE1:28, REWRITE1:31;
hence the reduction of X reduces b,a by REWRITE1:12; :: thesis: verum

end;

end;

end;

assume B1: for a, b being object st a is_a_normal_form_wrt the reduction of X & a,b are_convertible_wrt the reduction of X holds
the reduction of X reduces b,a ; :: according to REWRITE1:def 20 :: thesis: X is N.F.
let x be Element of X; :: according to ABSRED_0:def 18 :: thesis: for y being Element of X st x is normform & x <=*=> y holds
y =*=> x
let y be Element of X; :: thesis: ( x is normform & x <=*=> y implies y =*=> x )
assume ( x is normform & x <=*=> y ) ; :: thesis: y =*=> x
hence the reduction of X reduces y,x by B1, Ch1; :: according to ABSRED_0:def 3 :: thesis: verum