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