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: 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 that
A2: Topology_of T c= Z and
A3: Z is SigmaField of T ; :: thesis: BT c= Z
reconsider Z9 = Z as SigmaField of T by A3;
Z9 is all-open-containing by A2, Th59;
hence BT c= Z by Def11; :: thesis: verum
end;
Topology_of T c= BT by Th65;
hence BorelSets T = sigma (Topology_of T) by A1, PROB_1:def 9; :: thesis: verum