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

assume A2: X0 is boundary ; :: thesis: contradiction
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
( A is boundary & A is open ) by A1, A2, Def3, TSEP_1:16;
then ( Int A = {} & Int A = A ) by TOPS_1:55, TOPS_1:84;
hence contradiction ; :: thesis: verum

end;

hence not X0 is boundary ; :: thesis: verum