theorem lemalph: :: FIELD_9:46

( - alpha = alpha & alpha " = alpha-1 & alpha " <> alpha )