for n being Nat st n >= 1 holds
for P being Subset of (Euclid n) st P is bounded holds
not P ` is bounded