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 ;
per cases ( ( A <> {} & B <> {} ) or A = {} or B = {} ) ;
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;
suppose A = {} ; :: thesis: A \/ B is F_sigma
hence A \/ B is F_sigma by A2; :: thesis: verum
end;
suppose B = {} ; :: thesis: A \/ B is F_sigma
hence A \/ B is F_sigma by A1; :: thesis: verum
end;
end;