let X be ARS ; :: thesis: for x, y, z being Element of X st y is_normform_of x & z is_normform_of x & y <> z holds
x =+=> y
let x, y, z be Element of X; :: thesis: ( y is_normform_of x & z is_normform_of x & y <> z implies x =+=> y )
assume A1: y is_normform_of x ; :: thesis: ( not z is_normform_of x or not y <> z or x =+=> y )
assume A2: z is_normform_of x ; :: thesis: ( not y <> z or x =+=> y )
assume A3: y <> z ; :: thesis: x =+=> y
A6: ( x = y or x =+=> y ) by A1, LemN;
thus x =+=> y by A3, A1, A2, A6, LemN1; :: thesis: verum