let A be Subset of T; :: thesis: ( A is F_sigma implies A is Borel )
assume A is F_sigma ; :: thesis: A is Borel
then consider F being countable closed Subset-Family of T such that
A1: A = union F by Def6;
F c= BorelSets T by Th68;
then A in BorelSets T by A1, Def4;
hence A is Borel by Def12; :: thesis: verum