set X = the strict discrete TopSpace;
take the strict discrete TopSpace ; :: thesis: ( the strict discrete TopSpace is almost_discrete & the strict discrete TopSpace is strict )
thus ( the strict discrete TopSpace is almost_discrete & the strict discrete TopSpace is strict ) ; :: thesis: verum