let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T st F is closed & G is closed holds

INTERSECTION (F,G) is closed

let F, G be Subset-Family of T; :: thesis: ( F is closed & G is closed implies INTERSECTION (F,G) is closed )

assume A1: ( F is closed & G is closed ) ; :: thesis: INTERSECTION (F,G) is closed

for A being Subset of T st A in INTERSECTION (F,G) holds

A is closed

INTERSECTION (F,G) is closed

let F, G be Subset-Family of T; :: thesis: ( F is closed & G is closed implies INTERSECTION (F,G) is closed )

assume A1: ( F is closed & G is closed ) ; :: thesis: INTERSECTION (F,G) is closed

for A being Subset of T st A in INTERSECTION (F,G) holds

A is closed

proof

hence
INTERSECTION (F,G) is closed
by TOPS_2:def 2; :: thesis: verum
let A be Subset of T; :: thesis: ( A in INTERSECTION (F,G) implies A is closed )

assume A in INTERSECTION (F,G) ; :: thesis: A is closed

then consider X, Y being set such that

A2: ( X in F & Y in G ) and

A3: A = X /\ Y by SETFAM_1:def 5;

reconsider X = X, Y = Y as Subset of T by A2;

( X is closed & Y is closed ) by A1, A2, TOPS_2:def 2;

hence A is closed by A3; :: thesis: verum

end;assume A in INTERSECTION (F,G) ; :: thesis: A is closed

then consider X, Y being set such that

A2: ( X in F & Y in G ) and

A3: A = X /\ Y by SETFAM_1:def 5;

reconsider X = X, Y = Y as Subset of T by A2;

( X is closed & Y is closed ) by A1, A2, TOPS_2:def 2;

hence A is closed by A3; :: thesis: verum