begin
begin
Lm1:
for T being non empty TopSpace
for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
begin
Lm2:
[#] R^1 <> {}
;
:: The Weierstrass` theorem
::