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 Th29;
then egy -th-polytope (p,(dim p)) = ((dim p) -polytope-seq p) . egy by Def12
.= p by A1, FINSEQ_1:40 ;
hence 1 -th-polytope (p,(dim p)) = p ; :: thesis: verum