reconsider F = {({} T)} as Subset-Family of T by ZFMISC_1:31;
A1: F is closed by TARSKI:def 1;
F is open by TARSKI:def 1;
hence ex b₁ being Subset-Family of T st
( b₁ is open & b₁ is closed & not b₁ is empty ) by A1; :: thesis: verum