let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
let X0 be SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is boundary iff A is boundary )
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies ( X0 is boundary iff A is boundary ) )
assume A1: A = the carrier of X0 ; :: thesis: ( X0 is boundary iff A is boundary )
hence ( X0 is boundary implies A is boundary ) by Def3; :: thesis: ( A is boundary implies X0 is boundary )
assume A is boundary ; :: thesis: X0 is boundary
then for B being Subset of X st B = the carrier of X0 holds
B is boundary by A1;
hence X0 is boundary by Def3; :: thesis: verum