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