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 dense holds
( C is dense & C is open )
let D be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to D) st C = D & D is dense holds
( C is dense & C is open )
let C be Subset of (X modified_with_respect_to D); :: thesis: ( C = D & D is dense implies ( C is dense & C is open ) )
assume A1: C = D ; :: thesis: ( not D is dense or ( C is dense & C is open ) )
assume A2: D is dense ; :: thesis: ( C is dense & C is open )
set A = (Cl C) ` ;
reconsider B = (Cl C) ` as Subset of X by TMAP_1:104;
(Cl C) ` in the topology of (X modified_with_respect_to D) by PRE_TOPC:def 5;
then (Cl C) ` in D -extension_of_the_topology_of X by TMAP_1:104;
then (Cl C) ` in { (H \/ (G /\ D)) where H, G is Subset of X : ( H in the topology of X & G in the topology of X ) } by TMAP_1:def 7;
then consider H, G being Subset of X such that
A3: (Cl C) ` = H \/ (G /\ D) and
A4: H in the topology of X and
G in the topology of X ;
A5: C c= Cl C by PRE_TOPC:48;
then ( D misses (Cl C) ` & G /\ D c= D ) by A1, SUBSET_1:44, XBOOLE_1:17;
then G /\ D misses (Cl C) ` by XBOOLE_1:63;
then A6: (G /\ D) /\ ((Cl C) ` ) = {} by XBOOLE_0:def 7;
(Cl C) ` = (H \/ (G /\ D)) /\ ((Cl C) ` ) by A3
.= (H /\ ((Cl C) ` )) \/ {} by A6, XBOOLE_1:23
.= H /\ ((Cl C) ` ) ;
then ( (Cl C) ` c= H & H c= (Cl C) ` ) by A3, XBOOLE_1:7, XBOOLE_1:17;
then B = H by XBOOLE_0:def 10;
then ( B is open & D misses B ) by A1, A4, A5, PRE_TOPC:def 5, SUBSET_1:44;
then ( Cl D misses B & Cl D = [#] X ) by A2, TOPS_1:def 3, TSEP_1:40;
then A7: ( (Cl D) /\ B = {} & Cl D = [#] X ) by XBOOLE_0:def 7;
thus C is dense :: thesis: C is open

proof

assume not C is dense ; :: thesis: contradiction
then Cl C <> [#] (X modified_with_respect_to D) by TOPS_1:def 3;
then B <> {} (X modified_with_respect_to D) by TOPS_3:2;
hence contradiction by A7, XBOOLE_1:28; :: thesis: verum

end;

thus C is open by A1, TMAP_1:105; :: thesis: verum