consider X0 being strict proper SubSpace of X;
take X0 ; :: thesis: ( not X0 is everywhere_dense & X0 is strict )
thus ( not X0 is everywhere_dense & X0 is strict ) ; :: thesis: verum