let S be TopSpace; :: thesis: for T being non empty TopSpace
for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let T be non empty TopSpace; :: thesis: for K being Basis of T
for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let K be Basis of T; :: thesis: for f being Function of S,T holds
( f is continuous iff for A being Subset of T st A in K holds
f " A is open )
let f be Function of S,T; :: thesis: ( f is continuous iff for A being Subset of T st A in K holds
f " A is open )

hereby :: thesis: ( ( for A being Subset of T st A in K holds
f " A is open ) implies f is continuous )

assume A1: f is continuous ; :: thesis: for A being Subset of T st A in K holds
f " A is open
let A be Subset of T; :: thesis: ( A in K implies f " A is open )
assume A in K ; :: thesis: f " A is open
then f " (A `) is closed by A1, Th33;
then (f " A) ` is closed by Th2;
hence f " A is open by TOPS_1:4; :: thesis: verum

end;

assume A2: for A being Subset of T st A in K holds
f " A is open ; :: thesis: f is continuous

now :: thesis: for A being Subset of T st A in K holds
f " (A `) is closed

let A be Subset of T; :: thesis: ( A in K implies f " (A `) is closed )
assume A in K ; :: thesis: f " (A `) is closed
then f " A is open by A2;
then (f " A) ` is closed by TOPS_1:4;
hence f " (A `) is closed by Th2; :: thesis: verum

end;

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