let T be non empty TopSpace; :: thesis: for A being Subset of T st A is open holds

A is G_delta

let A be Subset of T; :: thesis: ( A is open implies A is G_delta )

assume A is open ; :: thesis: A is G_delta

then reconsider F = {A} as countable open Subset-Family of T by Th19;

take F ; :: according to TOPGEN_4:def 7 :: thesis: A = meet F

thus A = meet F by SETFAM_1:10; :: thesis: verum

A is G_delta

let A be Subset of T; :: thesis: ( A is open implies A is G_delta )

assume A is open ; :: thesis: A is G_delta

then reconsider F = {A} as countable open Subset-Family of T by Th19;

take F ; :: according to TOPGEN_4:def 7 :: thesis: A = meet F

thus A = meet F by SETFAM_1:10; :: thesis: verum