let T be non empty TopSpace; :: thesis: for F, G being Subset-Family of T st F is open & G is open holds
UNION (F,G) is open
let F, G be Subset-Family of T; :: thesis: ( F is open & G is open implies UNION (F,G) is open )
assume A1: ( F is open & G is open ) ; :: thesis: UNION (F,G) is open
for A being Subset of T st A in UNION (F,G) holds
A is open
proof
let A be Subset of T; :: thesis: ( A in UNION (F,G) implies A is open )
assume A in UNION (F,G) ; :: thesis: A is open
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 T by A2;
( X is open & Y is open ) by A1, A2, TOPS_2:def 1;
hence A is open by A3; :: thesis: verum
end;
hence UNION (F,G) is open by TOPS_2:def 1; :: thesis: verum