q is n + 0 -element ;
hence p (#) q is n -element ; :: thesis: verum