let X be ARS ; :: thesis: ( X is UN implies X is UN* )

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: X is UN*

let x be Element of X; :: according to ABSRED_0:def 16 :: thesis: for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z

let y, z be Element of X; :: thesis: ( y is_normform_of x & z is_normform_of x implies y = z )

assume A2: ( y is normform & x =*=> y ) ; :: according to ABSRED_0:def 12 :: thesis: ( not z is_normform_of x or y = z )

assume A3: ( z is normform & x =*=> z ) ; :: according to ABSRED_0:def 12 :: thesis: y = z

A4: ( x <=*=> y & x <=*=> z ) by A2, A3, LemZ;

thus y = z by A1, A2, A3, A4, Th7; :: thesis: verum

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: X is UN*

let x be Element of X; :: according to ABSRED_0:def 16 :: thesis: for y, z being Element of X st y is_normform_of x & z is_normform_of x holds

y = z

let y, z be Element of X; :: thesis: ( y is_normform_of x & z is_normform_of x implies y = z )

assume A2: ( y is normform & x =*=> y ) ; :: according to ABSRED_0:def 12 :: thesis: ( not z is_normform_of x or y = z )

assume A3: ( z is normform & x =*=> z ) ; :: according to ABSRED_0:def 12 :: thesis: y = z

A4: ( x <=*=> y & x <=*=> z ) by A2, A3, LemZ;

thus y = z by A1, A2, A3, A4, Th7; :: thesis: verum