let NTX, NTY be NTopSpace; :: thesis: for f being Function of NTX,NTY holds
( f is continuous iff for O being open Subset of NTY holds f " O is open Subset of NTX )
let f be Function of NTX,NTY; :: thesis: ( f is continuous iff for O being open Subset of NTY holds f " O is open Subset of NTX )

hereby :: thesis: ( ( for O being open Subset of NTY holds f " O is open Subset of NTX ) implies f is continuous )

assume f is continuous ; :: thesis: for O being open Subset of NTY holds f " O is open Subset of NTX
then for A being Subset of NTX holds f .: (Cl A) c= Cl (f .: A) by Lm13;
then for S being closed Subset of NTY holds f " S is closed Subset of NTX by Lm23;
hence for O being open Subset of NTY holds f " O is open Subset of NTX by Lm24; :: thesis: verum

end;

assume for O being open Subset of NTY holds f " O is open Subset of NTX ; :: thesis: f is continuous
hence f is continuous by Lm26; :: thesis: verum