let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is open holds
for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let f be Function of S,T; :: thesis: ( f is open implies for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P )
assume A1: for A being Subset of S st A is open holds
f .: A is open ; :: according to T_0TOPSP:def 2 :: thesis: for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let p be Point of S; :: thesis: for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let P be a_neighborhood of p; :: thesis: ex R being open a_neighborhood of f . p st R c= f .: P
A2: p in Int P by CONNSP_2:def 1;
f .: (Int P) is open by A1;
then reconsider R = f .: (Int P) as open a_neighborhood of f . p by A2, CONNSP_2:3, FUNCT_2:35;
take R ; :: thesis: R c= f .: P
thus R c= f .: P by RELAT_1:123, TOPS_1:16; :: thesis: verum