let p be polyhedron; :: thesis: for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
let k be Integer; :: thesis: ( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
set X = k -polytopes p;
thus ( not k -polytopes p is empty implies ( - 1 <= k & k <= dim p ) ) by Def5; :: thesis: ( - 1 <= k & k <= dim p implies not k -polytopes p is empty )
thus ( - 1 <= k & k <= dim p implies not k -polytopes p is empty ) :: thesis: verum

proof

assume A1: - 1 <= k ; :: thesis: ( not k <= dim p or not k -polytopes p is empty )
assume A2: k <= dim p ; :: thesis: not k -polytopes p is empty

per cases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A1, A2, XXREAL_0:1;

suppose k = - 1 ; :: thesis: not k -polytopes p is empty

hence not k -polytopes p is empty by Def5; :: thesis: verum

end;

suppose A3: ( - 1 < k & k < dim p ) ; :: thesis: not k -polytopes p is empty

set F = the PolytopsF of p;
A4: k -polytopes p = rng (the PolytopsF of p . (k + 1)) by A3, Def5;
set n = k + 1;
A5: 1 <= k + 1 by A3, Th25;
A6: k + 1 <= dim p by A3, Th25;
reconsider n = k + 1 as Element of NAT by A5, INT_1:16;
reconsider n = n as Nat ;
( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) by A5, A6, Def3;
hence not k -polytopes p is empty by A4; :: thesis: verum

end;

suppose k = dim p ; :: thesis: not k -polytopes p is empty

then k -polytopes p = {p} by Def5;
hence not k -polytopes p is empty ; :: thesis: verum

end;

end;

end;