let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let X0 be non empty SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let C, A be Subset of X; :: thesis: for B being Subset of X0 st C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary holds
B is boundary
let B be Subset of X0; :: thesis: ( C is open & C c= the carrier of X0 & A c= C & A = B & A is boundary implies B is boundary )
assume ( C is open & C c= the carrier of X0 & A c= C & A = B ) ; :: thesis: ( not A is boundary or B is boundary )
then A1: Int A = Int B by Th57;
assume A is boundary ; :: thesis: B is boundary
then Int A = {} ;
hence B is boundary by A1, TOPS_1:48; :: thesis: verum