let T be non empty TopSpace; :: thesis: for F being open Subset-Family of T holds F c= BorelSets T

let F be open Subset-Family of T; :: thesis: F c= BorelSets T

F c= BorelSets T

let F be open Subset-Family of T; :: thesis: F c= BorelSets T

F c= BorelSets T

proof

hence
F c= BorelSets T
; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in BorelSets T )

assume A1: x in F ; :: thesis: x in BorelSets T

then reconsider xx = x as Subset of T ;

xx is open by A1, TOPS_2:def 1;

hence x in BorelSets T by Def2; :: thesis: verum

end;assume A1: x in F ; :: thesis: x in BorelSets T

then reconsider xx = x as Subset of T ;

xx is open by A1, TOPS_2:def 1;

hence x in BorelSets T by Def2; :: thesis: verum