a 'nor' b is Element of Funcs Y,BOOLEAN ;
hence a 'nor' b is Element of Funcs Y,BOOLEAN ; :: thesis: verum