let T, S be TopStruct ; :: thesis: for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is closed holds
for F being Subset-Family of T st F = (" f) .: H holds
F is closed
let f be Function of T,S; :: thesis: for H being Subset-Family of S st f is continuous & H is closed holds
for F being Subset-Family of T st F = (" f) .: H holds
F is closed
let H be Subset-Family of S; :: thesis: ( f is continuous & H is closed implies for F being Subset-Family of T st F = (" f) .: H holds
F is closed )
assume that
A1: f is continuous and
A2: H is closed ; :: thesis: for F being Subset-Family of T st F = (" f) .: H holds
F is closed
let F be Subset-Family of T; :: thesis: ( F = (" f) .: H implies F is closed )
assume A3: F = (" f) .: H ; :: thesis: F is closed
let X be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( X in F implies X is closed )
assume X in F ; :: thesis: X is closed
then consider y being object such that
A4: y in dom (" f) and
A5: y in H and
A6: X = (" f) . y by A3, FUNCT_1:def 6;
reconsider Y = y as Subset of S by A5;
A7: X = f " Y by A4, A6, FUNCT_3:21;
Y is closed by A2, A5;
hence X is closed by A1, A7; :: thesis: verum