:: deftheorem Def11 defines BorelSets TOPGEN_4:def 11 :
for T being non empty TopSpace
for b₂ being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds
( b₂ = BorelSets T iff for G being compl-closed all-open-containing closed_for_countable_unions Subset-Family of T holds b₂ c= G );