let NTX, NTY be NTopSpace; :: thesis: for f being Function of NTX,NTY st ( for S being closed Subset of NTY holds f " S is closed Subset of NTX ) holds
for S being open Subset of NTY holds f " S is open Subset of NTX
let f be Function of NTX,NTY; :: thesis: ( ( for S being closed Subset of NTY holds f " S is closed Subset of NTX ) implies for S being open Subset of NTY holds f " S is open Subset of NTX )
assume A1: for S being closed Subset of NTY holds f " S is closed Subset of NTX ; :: thesis: for S being open Subset of NTY holds f " S is open Subset of NTX

now :: thesis: for S being open Subset of NTY holds f " S is open Subset of NTX

let S be open Subset of NTY; :: thesis: f " S is open Subset of NTX
reconsider NS = ([#] NTY) \ S as closed Subset of NTY by XBOOLE_1:36, Lm6;
reconsider fNS = f " NS as closed Subset of NTX by A1;
fNS = (f " ([#] NTY)) \ (f " S) by FUNCT_1:69
.= ([#] NTX) \ (f " S) by FUNCT_2:40 ;
then ([#] NTX) \ fNS = ([#] NTX) /\ (f " S) by XBOOLE_1:48;
then f " S = ([#] NTX) \ fNS by XBOOLE_1:28;
hence f " S is open Subset of NTX by Lm8; :: thesis: verum

end;

hence for S being open Subset of NTY holds f " S is open Subset of NTX ; :: thesis: verum