let Am be Subset of TM; :: thesis: ( Am is closed implies Am is G_delta )
assume A24: Am is closed ; :: thesis: Am is G_delta

per cases ( TM is empty or not TM is empty ) ;

suppose A25: TM is empty ; :: thesis: Am is G_delta

reconsider E = {} as empty Subset-Family of TM by TOPGEN_4:18;
Am = meet E by A25, SETFAM_1:1;
hence Am is G_delta by TOPGEN_4:def 7; :: thesis: verum

end;

suppose not TM is empty ; :: thesis: Am is G_delta

then (Am `) ` is G_delta by A24, TOPGEN_4:37;
hence Am is G_delta ; :: thesis: verum

end;

end;