for x being Complex holds
( not x ^2 = 1 or x = 1 or x = - 1 )