let T be non empty TopSpace; :: thesis: [#] T is G_delta

reconsider F = {([#] T)} as Subset-Family of T ;

( F is open & [#] T = meet F ) by Th19, SETFAM_1:10;

hence [#] T is G_delta ; :: thesis: verum

reconsider F = {([#] T)} as Subset-Family of T ;

( F is open & [#] T = meet F ) by Th19, SETFAM_1:10;

hence [#] T is G_delta ; :: thesis: verum