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