consider X0 being strict proper SubSpace of X;
take X0 ; :: thesis: ( X0 is discrete & X0 is open & X0 is closed & X0 is proper & X0 is strict )
thus ( X0 is discrete & X0 is open & X0 is closed & X0 is proper & X0 is strict ) ; :: thesis: verum