let X be ARS ; :: thesis: for x being Element of X st X is WN & X is UN* holds
nf x is normform
let x be Element of X; :: thesis: ( X is WN & X is UN* implies nf x is normform )
assume A1: ( X is WN & X is UN* ) ; :: thesis: nf x is normform
A2: nf x is_normform_of x by A1, Lem22;
thus nf x is normform by A2; :: thesis: verum