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

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

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

end;

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