let X be ARS ; :: thesis: ( X is UN iff the reduction of X is with_UN_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 UN implies the reduction of X is with_UN_property ) :: thesis: ( the reduction of X is with_UN_property implies X is UN )

proof

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

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: a = b

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

end;

suppose ( not a in the carrier of X or not b in the carrier of X ) ; :: thesis: a = b

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

end;

end;

end;

assume A4: for a, b being object st a is_a_normal_form_wrt the reduction of X & b is_a_normal_form_wrt the reduction of X & a,b are_convertible_wrt the reduction of X holds
a = b ; :: according to REWRITE1:def 19 :: thesis: X is UN
let x be Element of X; :: according to ABSRED_0:def 17 :: thesis: for y being Element of X st x is normform & y is normform & x <=*=> y holds
x = y
let y be Element of X; :: thesis: ( x is normform & y is normform & x <=*=> y implies x = y )
assume ( x is normform & y is normform & x <=*=> y ) ; :: thesis: x = y
then ( x is_a_normal_form_wrt the reduction of X & y is_a_normal_form_wrt the reduction of X & x,y are_convertible_wrt the reduction of X ) by Ch1;
hence x = y by A4; :: thesis: verum