theorem Th16: :: PSCOMP_1:16

for T being non empty TopSpace
for X being non empty Subset of T
for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
lower_bound (f | Y) <= lower_bound (f | X)