let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let A be Subset of X; :: thesis: for B being Subset of X0 st A c= B & B is boundary holds
A is boundary
let B be Subset of X0; :: thesis: ( A c= B & B is boundary implies A is boundary )
assume A1: A c= B ; :: thesis: ( not B is boundary or A is boundary )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume Int B = {} ; :: according to TOPS_3:def 1 :: thesis: A is boundary
then Int C = {} by A1, TOPS_1:48, XBOOLE_1:3;
then Int A = {} by Th56, XBOOLE_1:3;
hence A is boundary by Def1; :: thesis: verum