let X0 be non empty SubSpace of X; :: thesis: ( X0 is open implies not X0 is boundary )
assume A1: X0 is open ; :: 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;
assume X0 is boundary ; :: thesis: contradiction
then A is boundary ;
then A2: Int A = {} ;
A is open by A1, TSEP_1:16;
hence contradiction by A2, TOPS_1:23; :: thesis: verum

end;

hence not X0 is boundary ; :: thesis: verum