let X be ARS ; :: thesis: ( 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 ; :: according to ABSRED_0:def 18 :: 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;

A5: y <=*=> z by A4, Th7;

thus y = z by A2, A1, A3, A5, LemN1; :: thesis: verum

assume A1: for x, y being Element of X st x is normform & x <=*=> y holds

y =*=> x ; :: according to ABSRED_0:def 18 :: 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;

A5: y <=*=> z by A4, Th7;

thus y = z by A2, A1, A3, A5, LemN1; :: thesis: verum