let X be non empty TopSpace; :: thesis: for A being Subset of X
for B being Subset of (X modified_with_respect_to A) st B = A holds
B is open
let A be Subset of X; :: thesis: for B being Subset of (X modified_with_respect_to A) st B = A holds
B is open
let B be Subset of (X modified_with_respect_to A); :: thesis: ( B = A implies B is open )
assume B = A ; :: thesis: B is open
then B in A -extension_of_the_topology_of X by Th102;
hence B is open by PRE_TOPC:def 2; :: thesis: verum