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 x2 being Point of T st
( x2 in P & f . x2 = lower_bound (f .: P) )