let T be TopStruct ; :: thesis: for f being RealMap of T
for R being Subset-Family of REAL st f is continuous & R is closed holds
(" f) .: R is closed
let f be RealMap of T; :: thesis: for R being Subset-Family of REAL st f is continuous & R is closed holds
(" f) .: R is closed
let R be Subset-Family of REAL; :: thesis: ( f is continuous & R is closed implies (" f) .: R is closed )
assume A1: f is continuous ; :: thesis: ( not R is closed or (" f) .: R is closed )
assume A2: R is closed ; :: thesis: (" f) .: R is closed
let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not P in (" f) .: R or P is closed )
assume P in (" f) .: R ; :: thesis: P is closed
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 closed by A2, A4;
hence P is closed by A1, A6; :: thesis: verum