consider A0 being non empty Subset of X such that
A1: A0 is boundary by TEX_1:def 5;
consider X0 being non empty strict SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0 ; :: thesis: ( X0 is boundary & X0 is strict & not X0 is empty )
for A being Subset of X st A = the carrier of X0 holds
A is boundary by A1, A2;
hence ( X0 is boundary & X0 is strict & not X0 is empty ) ; :: thesis: verum