let T be TopStruct ; :: thesis: for M being Subset of T
for F being Subset-Family of T st F is open holds
F | M is open
let M be Subset of T; :: thesis: for F being Subset-Family of T st F is open holds
F | M is open
let F be Subset-Family of T; :: thesis: ( F is open implies F | M is open )
assume A1: F is open ; :: thesis: F | M is open
let Q be Subset of (T | M); :: according to TOPS_2:def 1 :: thesis: ( Q in F | M implies Q is open )
assume Q in F | M ; :: thesis: Q is open
then consider R being Subset of T such that
A2: R in F and
A3: R /\ M = Q by Def3;
reconsider R = R as Subset of T ;
A4: Q = R /\ ([#] (T | M)) by A3, PRE_TOPC:def 5;
R is open by A1, A2;
hence Q is open by A4, Th24; :: thesis: verum