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