let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A is F_sigma & B is F_sigma holds

A \/ B is F_sigma

let A, B be Subset of T; :: thesis: ( A is F_sigma & B is F_sigma implies A \/ B is F_sigma )

assume that

A1: A is F_sigma and

A2: B is F_sigma ; :: thesis: A \/ B is F_sigma

consider F being countable closed Subset-Family of T such that

A3: A = union F by A1;

consider G being countable closed Subset-Family of T such that

A4: B = union G by A2;

reconsider H = UNION (F,G) as Subset-Family of T ;

A \/ B is F_sigma

let A, B be Subset of T; :: thesis: ( A is F_sigma & B is F_sigma implies A \/ B is F_sigma )

assume that

A1: A is F_sigma and

A2: B is F_sigma ; :: thesis: A \/ B is F_sigma

consider F being countable closed Subset-Family of T such that

A3: A = union F by A1;

consider G being countable closed Subset-Family of T such that

A4: B = union G by A2;

reconsider H = UNION (F,G) as Subset-Family of T ;

per cases
( ( A <> {} & B <> {} ) or A = {} or B = {} )
;

end;

suppose A5:
( A <> {} & B <> {} )
; :: thesis: A \/ B is F_sigma

A6:
H is closed
by Th22;

( card H c= card [:F,G:] & [:F,G:] is countable ) by Th26, CARD_4:7;

then A7: H is countable by WAYBEL12:1;

A \/ B = union H by A3, A4, A5, Th28, ZFMISC_1:2;

hence A \/ B is F_sigma by A6, A7; :: thesis: verum

end;( card H c= card [:F,G:] & [:F,G:] is countable ) by Th26, CARD_4:7;

then A7: H is countable by WAYBEL12:1;

A \/ B = union H by A3, A4, A5, Th28, ZFMISC_1:2;

hence A \/ B is F_sigma by A6, A7; :: thesis: verum