let p be polyhedron; :: thesis: {p} is Element of
(dim p) -polytopes p = {p} by Def5;
hence {p} is Element of by ZFMISC_1:def 1; :: thesis: verum