reconsider a = a as Function of Y,BOOLEAN ;
'not' a is Function of Y,BOOLEAN ;
hence 'not' a is Function of Y,BOOLEAN ; :: thesis: verum