set X = the non empty strict discrete anti-discrete TopStruct ;
reconsider X = the non empty strict discrete anti-discrete TopStruct as TopSpace ;
take X ; :: thesis: ( X is discrete & X is anti-discrete & X is strict & not X is empty )
thus ( X is discrete & X is anti-discrete & X is strict & not X is empty ) ; :: thesis: verum