begin
Lm1:
for X being Subset of REAL st X is bounded_below holds
-- X is bounded_above
Lm2:
for X being non empty set
for f being Function of X,REAL st f is with_min holds
- f is with_max
begin
begin
begin
Lm3:
for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )