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