let n be Nat; :: thesis: for B being non empty Subset of (TOP-REAL n)
for A being Subset of (TOP-REAL n)
for a being Real st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B holds
(TOP-REAL n) | B is locally_connected
let B be non empty Subset of (TOP-REAL n); :: thesis: for A being Subset of (TOP-REAL n)
for a being Real st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B holds
(TOP-REAL n) | B is locally_connected
let A be Subset of (TOP-REAL n); :: thesis: for a being Real st A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B holds
(TOP-REAL n) | B is locally_connected
let a be Real; :: thesis: ( A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B implies (TOP-REAL n) | B is locally_connected )
assume A1: ( A = { q where q is Point of (TOP-REAL n) : |.q.| = a } & A ` = B ) ; :: thesis: (TOP-REAL n) | B is locally_connected
then A ` is open by Th64;
hence (TOP-REAL n) | B is locally_connected by A1, Th65; :: thesis: verum