consider A being non empty Subset of X such that
A1:
A is nowhere_dense
by TEX_1:def 6;
consider C being Subset of X such that
A2:
A c= C
and
A3:
( C is closed & C is boundary )
by A1, TOPS_3:27;
not C is empty
by A2, XBOOLE_1:3;
then consider X0 being non empty strict SubSpace of X such that
A4:
C = the carrier of X0
by TSEP_1:10;
take
X0
; ( X0 is boundary & X0 is closed & X0 is strict & not X0 is empty )
( ( for C being Subset of X st C = the carrier of X0 holds
C is boundary ) & ( for C being Subset of X st C = the carrier of X0 holds
C is closed ) )
by A3, A4;
hence
( X0 is boundary & X0 is closed & X0 is strict & not X0 is empty )
by BORSUK_1:def 11; verum