let T be TopStruct ; :: thesis: 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
let f be RealMap of T; :: thesis: for R being Subset-Family of REAL st f is continuous & R is open holds
(" f) .: R is open
let R be Subset-Family of REAL ; :: thesis: ( f is continuous & R is open implies (" f) .: R is open )
assume A1: f is continuous ; :: thesis: ( not R is open or (" f) .: R is open )
assume A2: R is open ; :: thesis: (" f) .: R is open
let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in (" f) .: R or P is open )
assume P in (" f) .: R ; :: thesis: P is open
then consider eR being set such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = (" f) . eR by FUNCT_2:115;
A6: P = f " eR by A3, A5, Def2;
reconsider eR = eR as Subset of REAL by A3;
eR is open by A2, A4, Def5;
hence P is open by A1, A6, Th54; :: thesis: verum