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 )
assume A1: X0 is boundary ; :: thesis: for A being Subset of X st A c= the carrier of X0 holds
A is boundary
let A be Subset of X; :: thesis: ( A c= the carrier of X0 implies A is boundary )
assume A2: A c= the carrier of X0 ; :: thesis: A is boundary
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
C is boundary by A1, Def3;
hence A is boundary by A2, TOPS_3:11; :: thesis: verum