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 Th72;
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 JORDAN5A:27;
then f .: (Cl P) is closed by A1, COMPTS_1:7, WEIERSTR:9;
then A2: g .: (Cl P) is closed by JORDAN5A:23;
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