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;