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