reconsider F = {({} T)} as Subset-Family of T by ZFMISC_1:37;
A1: F is open

proof

let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in F or P is open )
assume P in F ; :: thesis: P is open
hence P is open by TARSKI:def 1; :: thesis: verum

end;

F is closed

proof

let P be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not P in F or P is closed )
assume P in F ; :: thesis: P is closed
hence P is closed by TARSKI:def 1; :: thesis: verum

end;

hence ex b₁ being Subset-Family of T st
( b₁ is open & b₁ is closed & not b₁ is empty ) by A1; :: thesis: verum