let X be ARS ; ( X is N.F. implies X is UN* )
assume A1:
for x, y being Element of X st x is normform & x <=*=> y holds
y =*=> x
; ABSRED_0:def 18 X is UN*
let x be Element of X; ABSRED_0:def 16 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; ( y is_normform_of x & z is_normform_of x implies y = z )
assume A2:
( y is normform & x =*=> y )
; ABSRED_0:def 12 ( not z is_normform_of x or y = z )
assume A3:
( z is normform & x =*=> z )
; ABSRED_0:def 12 y = z
A4:
( x <=*=> y & x <=*=> z )
by A2, A3, LemZ;
A5:
y <=*=> z
by A4, Th7;
thus
y = z
by A2, A1, A3, A5, LemN1; verum