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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (G | B) or x in F )
assume A5: x in meet (G | B) ; :: thesis: x in F
then consider g being object such that
A6: g in G | B by SETFAM_1:1, XBOOLE_0:def 1;
reconsider g = g as Subset of (T | B) by A6;
A7: ex h being Subset of T st
( h in G & h /\ B = g ) by A6, TOPS_2:def 3;
x in g by A5, A6, SETFAM_1:def 1;
then A8: x in B by A7, XBOOLE_0:def 4;

now :: thesis: for Y being set st Y in G holds
x in Y

let Y be set ; :: thesis: ( Y in G implies x in Y )
assume Y in G ; :: thesis: x in Y
then Y /\ B in G | B by TOPS_2:31;
then x in Y /\ B by A5, SETFAM_1:def 1;
hence x in Y by XBOOLE_0:def 4; :: thesis: verum

end;

then x in A by A3, A7, SETFAM_1:def 1;
hence x in F by A2, A8, 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 A9: ( G | B is open & G | B is countable ) by TOPS_2:37;
F c= meet (G | B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in meet (G | B) )
assume A10: x in F ; :: thesis: x in meet (G | B)
then A11: x in A by A2, XBOOLE_0:def 4;
A12: x in B by A2, A10, XBOOLE_0:def 4;

A13: now :: thesis: for f being set st f in G | B holds
x in f

let f be set ; :: thesis: ( f in G | B implies x in f )
assume f in G | B ; :: thesis: x in f
then consider h being Subset of T such that
A14: h in G and
A15: h /\ B = f by TOPS_2:def 3;
x in h by A3, A11, A14, SETFAM_1:def 1;
hence x in f by A12, A15, XBOOLE_0:def 4; :: thesis: verum

end;

ex y being object st y in G by A3, A11, SETFAM_1:1, XBOOLE_0:def 1;
then not G | B is empty by TOPS_2:31;
hence x in meet (G | B) by A13, SETFAM_1:def 1; :: thesis: verum

end;

then F = meet (G | B) by A4;
hence F is G_delta by A9, TOPGEN_4:def 7; :: thesis: verum