let X be non empty TopSpace; :: thesis: for D being Subset of X
for C being Subset of (X modified_with_respect_to (D ` )) st C = D & D is boundary holds
( C is boundary & C is closed )
let D be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to (D ` )) st C = D & D is boundary holds
( C is boundary & C is closed )
let C be Subset of (X modified_with_respect_to (D ` )); :: thesis: ( C = D & D is boundary implies ( C is boundary & C is closed ) )
assume C = D ; :: thesis: ( not D is boundary or ( C is boundary & C is closed ) )
then A1: C ` = D ` by TMAP_1:104;
assume D is boundary ; :: thesis: ( C is boundary & C is closed )
then D ` is dense by TOPS_1:def 4;
then ( C ` is dense & C ` is open ) by A1, Th4;
hence ( C is boundary & C is closed ) by TOPS_1:29, TOPS_1:def 4; :: thesis: verum