a 'nand' b is Element of Funcs (Y,BOOLEAN) ;
hence a 'nand' b is Element of Funcs (Y,BOOLEAN) ; :: thesis: verum