let A be Subset of T; :: thesis: ( A is G_delta implies A is Borel )
assume A is G_delta ; :: thesis: A is Borel
then consider F being countable open Subset-Family of T such that
A1: A = meet F by Def7;
F c= BorelSets T by Th69;
then A in BorelSets T by A1, Def5;
hence A is Borel by Def12; :: thesis: verum