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 )

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

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 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
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

end;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 )
;

end;

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;( x is normform & y is normform & x <=*=> y ) by A2, Ch1;

hence a = b by A1; :: thesis: verum

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;hence a = b by A2, REWRITE1:28, REWRITE1:31; :: thesis: verum

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