let X be ARS ; :: thesis: for x, y being Element of X st x is normform & x =*=> y holds
x = y
let x, y be Element of X; :: thesis: ( x is normform & x =*=> y implies x = y )
assume A1: x is normform ; :: thesis: ( not x =*=> y or x = y )
assume A2: x =*=> y ; :: thesis: x = y
A4: not x =+=> y by A1;
thus x = y by A2, A4, LemN; :: thesis: verum