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 = INTERSECTION (F,G) as Subset-Family of T ;

A5: H is closed by Th21;

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

then A6: H is countable by WAYBEL12:1;

A /\ B = union H by A3, A4, SETFAM_1:28;

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

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 = INTERSECTION (F,G) as Subset-Family of T ;

A5: H is closed by Th21;

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

then A6: H is countable by WAYBEL12:1;

A /\ B = union H by A3, A4, SETFAM_1:28;

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