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 ;

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 = {} )
;

end;