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

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