consider X0 being non empty strict SubSpace of X;
take X0 ; :: thesis: ( not X0 is nowhere_dense & X0 is strict & not X0 is empty )
thus ( not X0 is nowhere_dense & X0 is strict & not X0 is empty ) ; :: thesis: verum