:: deftheorem defines Borel TOPGEN_4:def 12 :
for T being non empty TopSpace
for A being Subset of T holds
( A is Borel iff A in BorelSets T );