let T be non empty TopSpace; :: thesis: [#] T is G_delta
reconsider F = {([#] T)} as Subset-Family of T ;
A1: F is open by Th19;
[#] T = meet F by SETFAM_1:11;
hence [#] T is G_delta by A1, Def7; :: thesis: verum