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 ) )
set A = (Cl C) ` ;
(Cl C) ` in the topology of (X modified_with_respect_to D) by PRE_TOPC:def 2;
then (Cl C) ` in D -extension_of_the_topology_of X by TMAP_1:93;
then A2: (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;
reconsider B = (Cl C) ` as Subset of X by TMAP_1:93;
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 by A2;
A5: H c= (Cl C) ` by A3, XBOOLE_1:7;
A6: C c= Cl C by PRE_TOPC:18;
then D misses (Cl C) ` by A1, SUBSET_1:24;
then G /\ D misses (Cl C) ` by XBOOLE_1:17, XBOOLE_1:63;
then A7: (G /\ D) /\ ((Cl C) `) = {} by XBOOLE_0:def 7;
(Cl C) ` = (H \/ (G /\ D)) /\ ((Cl C) `) by A3
.= (H /\ ((Cl C) `)) \/ {} by A7, XBOOLE_1:23
.= H /\ ((Cl C) `) ;
then (Cl C) ` c= H by XBOOLE_1:17;
then B = H by A5, XBOOLE_0:def 10;
then A8: B is open by A4;
D misses B by A1, A6, SUBSET_1:24;
then Cl D misses B by A8, TSEP_1:36;
then A9: (Cl D) /\ B = {} by XBOOLE_0:def 7;
assume D is dense ; :: thesis: ( C is dense & C is open )
then A10: Cl D = [#] X by TOPS_1:def 3;
thus C is dense :: thesis: C is open thus C is open by A1, TMAP_1:94; :: thesis: verum