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:24;
f is continuous by Th83;
then f .: (Cl P) is closed by A1, COMPTS_1:16, WEIERSTR:15;
then A2: g .: (Cl P) is closed by Th79;
g .: P c= g .: (Cl P) by PRE_TOPC:48, RELAT_1:156;
hence Cl (g .: P) c= g .: (Cl P) by A2, PSCOMP_1:32; :: thesis: verum