set F = the PolytopsF of p;
let X, Y be finite set ; :: thesis: ( ( k < - 1 implies X = {} ) & ( k = - 1 implies X = {{}} ) & ( - 1 < k & k < dim p implies X = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies X = {p} ) & ( k > dim p implies X = {} ) & ( k < - 1 implies Y = {} ) & ( k = - 1 implies Y = {{}} ) & ( - 1 < k & k < dim p implies Y = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies Y = {p} ) & ( k > dim p implies Y = {} ) implies X = Y )
assume that
A6: ( k < - 1 implies X = {} ) and
A7: ( k = - 1 implies X = {{}} ) and
A8: ( - 1 < k & k < dim p implies X = rng ( the PolytopsF of p . (k + 1)) ) and
A9: ( k = dim p implies X = {p} ) and
A10: ( k > dim p implies X = {} ) and
A11: ( k < - 1 implies Y = {} ) and
A12: ( k = - 1 implies Y = {{}} ) and
A13: ( - 1 < k & k < dim p implies Y = rng ( the PolytopsF of p . (k + 1)) ) and
A14: ( k = dim p implies Y = {p} ) and
A15: ( k > dim p implies Y = {} ) ; :: thesis: X = Y

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

suppose k < - 1 ; :: thesis: X = Y

hence X = Y by A6, A11; :: thesis: verum

end;

suppose k = - 1 ; :: thesis: X = Y

hence X = Y by A7, A12; :: thesis: verum

end;

suppose ( - 1 < k & k < dim p ) ; :: thesis: X = Y

hence X = Y by A8, A13; :: thesis: verum

end;

suppose k = dim p ; :: thesis: X = Y

hence X = Y by A9, A14; :: thesis: verum

end;

suppose k > dim p ; :: thesis: X = Y

hence X = Y by A10, A15; :: thesis: verum

end;

end;