reconsider a = a, b = b as Function of Y,BOOLEAN ;
a '&' b is Function of Y,BOOLEAN ;
hence a '&' b is Function of Y,BOOLEAN ; :: thesis: verum