let T be non empty TopSpace; :: thesis: for F being closed Subset-Family of T holds F c= BorelSets T
let F be closed Subset-Family of T; :: thesis: F c= BorelSets T
F c= BorelSets T
proof
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 closed by A1, TOPS_2:def 2;
hence x in BorelSets T by Def3; :: thesis: verum
end;
hence F c= BorelSets T ; :: thesis: verum