let T be TopSpace; :: thesis: for A, B being Subset of T
for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds
F is F_sigma
let A, B be Subset of T; :: thesis: for F being Subset of (T | B) st A is F_sigma & F = A /\ B holds
F is F_sigma
let F be Subset of (T | B); :: thesis: ( A is F_sigma & F = A /\ B implies F is F_sigma )
assume that
A1: A is F_sigma and
A2: F = A /\ B ; :: thesis: F is F_sigma
consider G being countable closed Subset-Family of T such that
A3: A = union G by A1, TOPGEN_4:def 6;
A4: union (G | B) c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (G | B) or x in F )
assume x in union (G | B) ; :: thesis: x in F
then consider g being set such that
A5: x in g and
A6: g in G | B by TARSKI:def 4;
consider h being Subset of T such that
A7: h in G and
A8: h /\ B = g by A6, TOPS_2:def 3;
x in h by A5, A8, XBOOLE_0:def 4;
then A9: x in A by A3, A7, TARSKI:def 4;
x in B by A5, A8, XBOOLE_0:def 4;
hence x in F by A2, A9, XBOOLE_0:def 4; :: thesis: verum

end;

( card (G | B) c= card G & card G c= omega ) by Th7, CARD_3:def 14;
then card (G | B) c= omega ;
then A10: ( G | B is closed & G | B is countable ) by TOPS_2:38;
(A /\ B) /\ B = A /\ (B /\ B) by XBOOLE_1:16
.= F by A2 ;
then F c= union (G | B) by A3, TOPS_2:32, XBOOLE_1:17;
then F = union (G | B) by A4;
hence F is F_sigma by A10, TOPGEN_4:def 6; :: thesis: verum