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