consider M being Subset of X such that
A1:
M is maximal_discrete
by Th60;
not M is empty
by A1, Th40;
then consider X0 being non empty strict SubSpace of X such that
A2:
X0 is maximal_discrete
and
M = the carrier of X0
by A1, Th47;
take
X0
; ( X0 is maximal_discrete & X0 is strict & not X0 is empty & not X0 is empty )
thus
( X0 is maximal_discrete & X0 is strict & not X0 is empty & not X0 is empty )
by A2; verum