let X be non empty TopSpace; :: thesis: for X0 being non empty open SubSpace of X
for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let X0 be non empty open SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let A be Subset of X; :: thesis: for B being Subset of X0 st A = B holds
( A is boundary iff B is boundary )
let B be Subset of X0; :: thesis: ( A = B implies ( A is boundary iff B is boundary ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A1: C is open by TSEP_1:def 1;
assume A = B ; :: thesis: ( A is boundary iff B is boundary )
hence ( A is boundary iff B is boundary ) by A1, Th65, Th66; :: thesis: verum