let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A is G_delta & B is G_delta holds
A \/ B is G_delta
let A, B be Subset of T; :: thesis: ( A is G_delta & B is G_delta implies A \/ B is G_delta )
assume that
A1: A is G_delta and
A2: B is G_delta ; :: thesis: A \/ B is G_delta
consider F being countable open Subset-Family of T such that
A3: A = meet F by A1;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2;
reconsider H = UNION (F,G) as Subset-Family of T ;
per cases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
suppose A5: ( F <> {} & G <> {} ) ; :: thesis: A \/ B is G_delta
A6: meet (UNION (F,G)) c= (meet F) \/ (meet G) by Th32;
(meet F) \/ (meet G) c= meet (UNION (F,G)) by A5, SETFAM_1:29;
then A7: A \/ B = meet H by A3, A4, A6;
( card H c= card [:F,G:] & [:F,G:] is countable ) by Th26, CARD_4:7;
then A8: H is countable by WAYBEL12:1;
H is open by Th24;
hence A \/ B is G_delta by A7, A8; :: thesis: verum
end;
suppose ( F = {} or G = {} ) ; :: thesis: A \/ B is G_delta
then ( A = {} or B = {} ) by A3, A4, SETFAM_1:def 1;
hence A \/ B is G_delta by A1, A2; :: thesis: verum
end;
end;