set F = {({} T)};

{({} T)} c= bool the carrier of T

take F ; :: thesis: ( not F is empty & F is mutually-disjoint & F is open & F is closed )

thus ( not F is empty & F is mutually-disjoint ) by TAXONOM2:10; :: thesis: ( F is open & F is closed )

thus F is open by TARSKI:def 1; :: thesis: F is closed

let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not P in F or P is closed )

thus ( not P in F or P is closed ) by TARSKI:def 1; :: thesis: verum

{({} T)} c= bool the carrier of T

proof

then reconsider F = {({} T)} as Subset-Family of T ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {({} T)} or a in bool the carrier of T )

assume a in {({} T)} ; :: thesis: a in bool the carrier of T

then a = {} T by TARSKI:def 1;

hence a in bool the carrier of T ; :: thesis: verum

end;assume a in {({} T)} ; :: thesis: a in bool the carrier of T

then a = {} T by TARSKI:def 1;

hence a in bool the carrier of T ; :: thesis: verum

take F ; :: thesis: ( not F is empty & F is mutually-disjoint & F is open & F is closed )

thus ( not F is empty & F is mutually-disjoint ) by TAXONOM2:10; :: thesis: ( F is open & F is closed )

thus F is open by TARSKI:def 1; :: thesis: F is closed

let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not P in F or P is closed )

thus ( not P in F or P is closed ) by TARSKI:def 1; :: thesis: verum