let T be TopStruct ; :: thesis: for F being Subset-Family of T
for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed
let F be Subset-Family of T; :: thesis: for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed
let A be SubSpace of T; :: thesis: ( F is closed implies for G being Subset-Family of A st G = F holds
G is closed )
assume A1: F is closed ; :: thesis: for G being Subset-Family of A st G = F holds
G is closed
let G be Subset-Family of A; :: thesis: ( G = F implies G is closed )
assume A2: G = F ; :: thesis: G is closed
let P be Subset of A; :: according to TOPS_2:def 2 :: thesis: ( P in G implies P is closed )
assume A3: P in G ; :: thesis: P is closed
reconsider PP = P as Subset of T by PRE_TOPC:11;
PP is closed by A1, A2, A3, Def2;
hence P is closed by Th34; :: thesis: verum