consider X being strict discrete TopSpace;
take X ; :: thesis: ( X is almost_discrete & X is strict )
thus ( X is almost_discrete & X is strict ) ; :: thesis: verum