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