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 set such that
A3: ( a in dom f & a in A & x = f . a ) by FUNCT_1:def 12;
reconsider p = a as Point of S by A3;
consider V being Subset of S such that
A4: ( V is open & V c= A & a in V ) by A2, A3;
V is a_neighborhood of p by A4, CONNSP_2:5;
then consider R being a_neighborhood of f . p such that
A5: R c= f .: V by A1, A4;
take K = Int R; :: thesis: ( K is open & K c= f .: A & x in K )
thus K is open ; :: thesis: ( K c= f .: A & x in K )
A6: f .: V c= f .: A by A4, RELAT_1:156;
Int R c= R by TOPS_1:44;
then K c= f .: V by A5, XBOOLE_1:1;
hence K c= f .: A by A6, XBOOLE_1:1; :: thesis: x in K
thus x in K by A3, 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:57; :: thesis: verum