let T be TopSpace; :: thesis: for S being non empty TopSpace
for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
let S be non empty TopSpace; :: thesis: for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )
let f be Function of T,S; :: thesis: ( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )

hereby :: thesis: ( ( for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P)
let P be Subset of T; :: thesis: f .: (Cl P) c= Cl (f .: P)
A2: Cl (f " (f .: P)) c= f " (Cl (f .: P)) by A1, Th56;
P c= [#] T ;
then P c= dom f by FUNCT_2:def 1;
then Cl P c= Cl (f " (f .: P)) by FUNCT_1:146, PRE_TOPC:49;
then Cl P c= f " (Cl (f .: P)) by A2, XBOOLE_1:1;
then A3: f .: (Cl P) c= f .: (f " (Cl (f .: P))) by RELAT_1:156;
f .: (f " (Cl (f .: P))) c= Cl (f .: P) by FUNCT_1:145;
hence f .: (Cl P) c= Cl (f .: P) by A3, XBOOLE_1:1; :: thesis: verum

end;

assume A4: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ; :: thesis: f is continuous

now

let P1 be Subset of S; :: thesis: Cl (f " P1) c= f " (Cl P1)
Cl (f " P1) c= [#] T ;
then Cl (f " P1) c= dom f by FUNCT_2:def 1;
then A5: Cl (f " P1) c= f " (f .: (Cl (f " P1))) by FUNCT_1:146;
f .: (f " P1) c= P1 by FUNCT_1:145;
then ( f .: (Cl (f " P1)) c= Cl (f .: (f " P1)) & Cl (f .: (f " P1)) c= Cl P1 ) by A4, PRE_TOPC:49;
then f .: (Cl (f " P1)) c= Cl P1 by XBOOLE_1:1;
then f " (f .: (Cl (f " P1))) c= f " (Cl P1) by RELAT_1:178;
hence Cl (f " P1) c= f " (Cl P1) by A5, XBOOLE_1:1; :: thesis: verum

end;

hence f is continuous by Th56; :: thesis: verum