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:93;
assume D is boundary ; :: thesis: ( C is boundary & C is closed )
then A2: D ` is dense by TOPS_1:def 4;
then A3: C ` is open by A1, Th4;
C ` is dense by A1, A2, Th4;
hence ( C is boundary & C is closed ) by A3, TOPS_1:def 4; :: thesis: verum