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 )
assume A2: B in the topology of X ; :: according to PRE_TOPC:def 5 :: thesis: C is open
( the topology of X c= D -extension_of_the_topology_of X & the topology of (X modified_with_respect_to D) = D -extension_of_the_topology_of X ) by TMAP_1:99, TMAP_1:104;
hence C is open by A1, A2, PRE_TOPC:def 5; :: thesis: verum