let p be polyhedron; :: thesis: 1 -th-polytope p,(dim p) = p
reconsider egy = 1 as Nat ;
set s = (dim p) -polytope-seq p;
A1: (dim p) -polytope-seq p = <*p*> by Def7;
egy <= num-polytopes p,(dim p) by Th32;
then egy -th-polytope p,(dim p) = ((dim p) -polytope-seq p) . egy by Def12
.= p by A1, FINSEQ_1:57 ;
hence 1 -th-polytope p,(dim p) = p ; :: thesis: verum