theorem :: TOPGRP_1:22
for S, T being non empty TopSpace
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