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