let T be TopStruct ; :: thesis: for M being Subset of T
for F being Subset-Family of T st F is closed holds
F | M is closed
let M be Subset of T; :: thesis: for F being Subset-Family of T st F is closed holds
F | M is closed
let F be Subset-Family of T; :: thesis: ( F is closed implies F | M is closed )
assume A1: F is closed ; :: thesis: F | M is closed
let Q be Subset of (T | M); :: according to TOPS_2:def 2 :: thesis: ( Q in F | M implies Q is closed )
assume Q in F | M ; :: thesis: Q is closed
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 closed by A1, A2;
hence Q is closed by A4, PRE_TOPC:13; :: thesis: verum