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

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

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

Topology_of T c= BT
by Th65;
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;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

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