let T be non empty TopSpace; :: thesis: BorelSets T = sigma (Topology_of T)
reconsider BT = BorelSets T as SigmaField of T by Th13;
set X = Topology_of T;
A1: Topology_of T c= BT by Th69;
for Z being set st Topology_of T c= Z & Z is SigmaField of T holds
BT c= Z

proof

let Z be set ; :: thesis: ( Topology_of T c= Z & Z is SigmaField of T implies BT c= Z )
assume A2: ( Topology_of T c= Z & Z is SigmaField of T ) ; :: thesis: BT c= Z
then reconsider Z' = Z as SigmaField of T ;
Z' is all-open-containing by A2, Th63;
hence BT c= Z by Def11; :: thesis: verum

end;

hence BorelSets T = sigma (Topology_of T) by A1, PROB_1:def 14; :: thesis: verum