let p be polyhedron; :: thesis: not 0 -polytopes p is empty
set d = dim p;
per cases ( dim p = 0 or dim p > 0 ) ;
suppose dim p = 0 ; :: thesis: not 0 -polytopes p is empty
then 0 -polytopes p = {p} by Def5;
hence not 0 -polytopes p is empty ; :: thesis: verum
end;
suppose dim p > 0 ; :: thesis: not 0 -polytopes p is empty
hence not 0 -polytopes p is empty by Th23; :: thesis: verum
end;
end;