let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X st X0 is boundary holds
for A being Subset of X st A c= the carrier of X0 holds
A is boundary
let X0 be SubSpace of X; :: thesis: ( X0 is boundary implies for A being Subset of X st A c= the carrier of X0 holds
A is boundary )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is boundary ; :: thesis: for A being Subset of X st A c= the carrier of X0 holds
A is boundary
then A1: C is boundary ;
let A be Subset of X; :: thesis: ( A c= the carrier of X0 implies A is boundary )
assume A c= the carrier of X0 ; :: thesis: A is boundary
hence A is boundary by A1, TOPS_3:11; :: thesis: verum