let X0 be SubSpace of X; :: thesis: ( X0 is everywhere_dense implies not X0 is boundary )
assume A3: X0 is everywhere_dense ; :: thesis: not X0 is boundary

now :: thesis: not X0 is boundary

reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A is everywhere_dense by A3;
then A4: not A is boundary by TOPS_3:37;
assume X0 is boundary ; :: thesis: contradiction
hence contradiction by A4; :: thesis: verum

end;

hence not X0 is boundary ; :: thesis: verum