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