let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) holds
f is open
let f be Function of S,T; :: thesis: ( ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) implies f is open )
assume A1: for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ; :: thesis: f is open
let A be Subset of S; :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or f .: A is open )
assume A2: A is open ; :: thesis: f .: A is open
for x being set holds
( x in f .: A iff ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) )

proof

let x be set ; :: thesis: ( x in f .: A iff ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) )

hereby :: thesis: ( ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )

assume x in f .: A ; :: thesis: ex K being Element of bool the carrier of T st
( K is open & K c= f .: A & x in K )
then consider a being object such that
A3: a in dom f and
A4: a in A and
A5: x = f . a by FUNCT_1:def 6;
reconsider p = a as Point of S by A3;
consider V being Subset of S such that
A6: V is open and
A7: V c= A and
A8: a in V by A2, A4;
V is a_neighborhood of p by A6, A8, CONNSP_2:3;
then consider R being a_neighborhood of f . p such that
A9: R c= f .: V by A1, A6;
take K = Int R; :: thesis: ( K is open & K c= f .: A & x in K )
Int R c= R by TOPS_1:16;
then A10: K c= f .: V by A9;
thus K is open ; :: thesis: ( K c= f .: A & x in K )
f .: V c= f .: A by A7, RELAT_1:123;
hence K c= f .: A by A10; :: thesis: x in K
thus x in K by A5, CONNSP_2:def 1; :: thesis: verum

end;

thus ( ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; :: thesis: verum

end;

hence f .: A is open by TOPS_1:25; :: thesis: verum