let X be non empty TopSpace; :: thesis: for D, B being Subset of X
for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds
C is open
let D, B be Subset of X; :: thesis: for C being Subset of (X modified_with_respect_to D) st B = C & B is open holds
C is open
let C be Subset of (X modified_with_respect_to D); :: thesis: ( B = C & B is open implies C is open )
assume A1: B = C ; :: thesis: ( not B is open or C is open )
A2: the topology of X c= D -extension_of_the_topology_of X by TMAP_1:88;
A3: the topology of (X modified_with_respect_to D) = D -extension_of_the_topology_of X by TMAP_1:93;
assume B in the topology of X ; :: according to PRE_TOPC:def 2 :: thesis: C is open
hence C is open by A1, A2, A3; :: thesis: verum