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