let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of st F is closed & G is closed holds
UNION F,G is closed
let F, G be Subset-Family of ; :: thesis: ( F is closed & G is closed implies UNION F,G is closed )
assume A1: ( F is closed & G is closed ) ; :: thesis: UNION F,G is closed
for A being Subset of st A in UNION F,G holds
A is closed

proof

let A be Subset of ; :: thesis: ( A in UNION F,G implies A is closed )
assume A in UNION 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 4;
reconsider X = X, Y = Y as Subset of by A2;
( X is closed & Y is closed ) by A1, A2, TOPS_2:def 2;
hence A is closed by A3; :: thesis: verum

end;

hence UNION F,G is closed by TOPS_2:def 2; :: thesis: verum