let NTX, NTY be NTopSpace; :: thesis: for f being Function of NTX,NTY st ( for A being Subset of NTX holds f .: (Cl A) c= Cl (f .: A) ) holds
for S being closed Subset of NTY holds f " S is closed Subset of NTX
let f be Function of NTX,NTY; :: thesis: ( ( for A being Subset of NTX holds f .: (Cl A) c= Cl (f .: A) ) implies for S being closed Subset of NTY holds f " S is closed Subset of NTX )
assume A1: for A being Subset of NTX holds f .: (Cl A) c= Cl (f .: A) ; :: thesis: for S being closed Subset of NTY holds f " S is closed Subset of NTX
let S9 be closed Subset of NTY; :: thesis: f " S9 is closed Subset of NTX
reconsider S = f " S9 as Subset of NTX ;
( f .: (Cl S) c= Cl (f .: S) & Cl (f .: S) c= Cl S9 ) by A1, Lm18, FUNCT_1:75;
then f .: (Cl S) c= Cl S9 ;
then f .: (Cl S) c= S9 by Lm20;
then A2: f " (f .: (Cl S)) c= f " S9 by RELAT_1:143;
dom f = [#] NTX by FUNCT_2:def 1;
then Cl S c= f " (f .: (Cl S)) by FUNCT_1:76;
then ( Cl S c= S & S c= Cl S ) by A2, Lm21;
then S = Cl S ;
hence f " S9 is closed Subset of NTX by Lm22; :: thesis: verum