for X being ARS st not X is CONF & X is WN holds
ex x, y, z being Element of X st
( y is_normform_of x & z is_normform_of x & y <> z )