let X be ARS ; :: thesis: for x, y being Element of X st X is WN & X is UN* & nf x = nf y holds
x <=*=> y
let x, y be Element of X; :: thesis: ( X is WN & X is UN* & nf x = nf y implies x <=*=> y )
assume A1: ( X is WN & X is UN* ) ; :: thesis: ( not nf x = nf y or x <=*=> y )
assume A2: nf x = nf y ; :: thesis: x <=*=> y
( nf x is_normform_of x & nf x is_normform_of y ) by A1, A2, Lem22;
then ( x <=*=> nf x & nf x <=*=> y ) by LemZ;
hence x <=*=> y by Th7; :: thesis: verum