consider X being non empty trivial strict TopSpace;
take X ; :: thesis: ( X is strict & X is T_0 & not X is empty )
thus ( X is strict & X is T_0 & not X is empty ) ; :: thesis: verum