let P be Subset of (TOP-REAL 2); :: thesis: ( P is Bounded implies for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P) )
assume P is Bounded ; :: thesis: for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P)
then A1: Cl P is compact by Th71, Th88;
let g be continuous RealMap of (TOP-REAL 2); :: thesis: Cl (g .: P) c= g .: (Cl P)
reconsider f = g as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
f is continuous by Th83;
then f .: (Cl P) is closed by A1, COMPTS_1:7, WEIERSTR:9;
then A2: g .: (Cl P) is closed by Th79;
g .: P c= g .: (Cl P) by PRE_TOPC:18, RELAT_1:123;
hence Cl (g .: P) c= g .: (Cl P) by A2, MEASURE6:57; :: thesis: verum