let X be ARS ; :: thesis: for x being Element of X st X is WN & X is UN* holds

nf (nf x) = nf x

let x be Element of X; :: thesis: ( X is WN & X is UN* implies nf (nf x) = nf x )

assume A1: ( X is WN & X is UN* ) ; :: thesis: nf (nf x) = nf x

A2: nf x is normform by A1, Lem24;

thus nf (nf x) = nf x by A1, A2, LemN2, Lem23; :: thesis: verum

nf (nf x) = nf x

let x be Element of X; :: thesis: ( X is WN & X is UN* implies nf (nf x) = nf x )

assume A1: ( X is WN & X is UN* ) ; :: thesis: nf (nf x) = nf x

A2: nf x is normform by A1, Lem24;

thus nf (nf x) = nf x by A1, A2, LemN2, Lem23; :: thesis: verum