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, Def7;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2, Def7;
reconsider H = UNION F,G as Subset-Family of T ;

per cases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;

suppose ( F <> {} & G <> {} ) ; :: thesis: A \/ B is G_delta

then A5: (meet F) \/ (meet G) c= meet (UNION F,G) by SETFAM_1:40;
meet (UNION F,G) c= (meet F) \/ (meet G) by Th32;
then A6: A \/ B = meet H by A3, A4, A5, XBOOLE_0:def 10;
A7: H is open by Th24;
A8: card H c= card [:F,G:] by Th26;
[:F,G:] is countable by CARD_4:55;
then H is countable by A8, WAYBEL12:2;
hence A \/ B is G_delta by A6, A7, Def7; :: 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;