theorem :: PSCOMP_1:12

for T being TopStruct
for f being RealMap of T
for R being Subset-Family of REAL st f is continuous & R is open holds
(" f) .: R is open