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