let X be non empty TopSpace; :: thesis: for A being Subset of
for B being Subset of st B = A holds
B is open
let A be Subset of ; :: thesis: for B being Subset of st B = A holds
B is open
let B be Subset of ; :: 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 5; :: thesis: verum