let T be non empty TopSpace; :: thesis: for A, B being Subset of T st A is G_delta & B is G_delta holds
A /\ B is G_delta
let A, B be Subset of T; :: thesis: ( A is G_delta & B is G_delta implies A /\ B is G_delta )
assume that
A1: A is G_delta and
A2: B is G_delta ; :: thesis: A /\ B is G_delta
consider F being countable open Subset-Family of T such that
A3: A = meet F by A1;
consider G being countable open Subset-Family of T such that
A4: B = meet G by A2;
reconsider H = INTERSECTION (F,G) as Subset-Family of T ;
per cases ( ( F <> {} & G <> {} ) or F = {} or G = {} ) ;
suppose A5: ( F <> {} & G <> {} ) ; :: thesis: A /\ B is G_delta
A6: H is open by Th23;
( card H c= card [:F,G:] & [:F,G:] is countable ) by Th25, CARD_4:7;
then A7: H is countable by WAYBEL12:1;
A /\ B = meet H by A3, A4, A5, Th34;
hence A /\ B is G_delta by A6, A7; :: thesis: verum
end;
suppose ( F = {} or G = {} ) ; :: thesis: A /\ B is G_delta
then ( A = {} or B = {} ) by A3, A4, SETFAM_1:def 1;
then A /\ B = {} T ;
hence A /\ B is G_delta ; :: thesis: verum
end;
end;