let T be TopStruct ; :: thesis: for F, G being Subset-Family of T st F c= G & G is closed holds
F is closed
let F, G be Subset-Family of T; :: thesis: ( F c= G & G is closed implies F is closed )
assume A1: ( F c= G & G is closed ) ; :: thesis: F is closed
let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( P in F implies P is closed )
assume P in F ; :: thesis: P is closed
hence P is closed by A1, Def2; :: thesis: verum