let S be TopSpace; :: thesis: for T being non empty TopSpace
for f being Function of S,T holds
( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) )
let T be non empty TopSpace; :: thesis: for f being Function of S,T holds
( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) )
let f be Function of S,T; :: thesis: ( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) )
A1: [#] T <> {} ;

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

assume A2: f is continuous ; :: thesis: for P being Subset of T holds f " (Int P) c= Int (f " P)
let P be Subset of T; :: thesis: f " (Int P) c= Int (f " P)
f " (Int P) c= f " P by RELAT_1:178, TOPS_1:44;
then A3: Int (f " (Int P)) c= Int (f " P) by TOPS_1:48;
f " (Int P) is open by A1, A2, TOPS_2:55;
hence f " (Int P) c= Int (f " P) by A3, TOPS_1:55; :: thesis: verum

end;

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

now

let P be Subset of T; :: thesis: ( P is open implies f " P is open )
assume P is open ; :: thesis: f " P is open
then Int P = P by TOPS_1:55;
then A5: f " P c= Int (f " P) by A4;
Int (f " P) c= f " P by TOPS_1:44;
hence f " P is open by A5, XBOOLE_0:def 10; :: thesis: verum

end;

hence f is continuous by A1, TOPS_2:55; :: thesis: verum