let X be ARS ; :: thesis: for x, y being Element of X st X is WN & X is UN* & x <=*=> y holds
nf x = nf y
let x, y be Element of X; :: thesis: ( X is WN & X is UN* & x <=*=> y implies nf x = nf y )
assume A1: ( X is WN & X is UN* ) ; :: thesis: ( not x <=*=> y or nf x = nf y )
assume A2: x <=*=> y ; :: thesis: nf x = nf y
defpred S₁[ Element of X] means nf x = nf $1;
A3: S₁[x] ;
A4: for z, u being Element of X st z <==> u & S₁[z] holds
S₁[u] by A1, Th2, Lem26;
S₁[y] from ABSRED_0:sch 6(A2, A3, A4);
hence nf x = nf y ; :: thesis: verum