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