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 ;

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 = {} )
;

end;

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;(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