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:143, TOPS_1:16;
then A3: Int (f " (Int P)) c= Int (f " P) by TOPS_1:19;
f " (Int P) is open by A1, A2, TOPS_2:43;
hence f " (Int P) c= Int (f " P) by A3, TOPS_1:23; :: thesis: verum

end;

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

now :: thesis: for P being Subset of T st P is open holds
f " P is open

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:23;
then A5: f " P c= Int (f " P) by A4;
Int (f " P) c= f " P by TOPS_1:16;
hence f " P is open by A5, XBOOLE_0:def 10; :: thesis: verum

end;

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