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 object such that
A3: eR in bool REAL and
A4: eR in R and
A5: P = (" f) . eR by FUNCT_2:64;
reconsider eR = eR as set by TARSKI:1;
A6: P = f " eR by A3, A5, MEASURE6:def 3;
reconsider eR = eR as Subset of REAL by A3;
eR is open by A2, A4;
hence P is open by A1, A6, Th8; :: thesis: verum