let T be non empty TopSpace; :: thesis: for S being non empty SubSpace of T
for A being non empty Subset of T
for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
let S be non empty SubSpace of T; :: thesis: for A being non empty Subset of T
for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
let A be non empty Subset of T; :: thesis: for B being non empty Subset of S st A = B & A is locally_connected holds
B is locally_connected
let B be non empty Subset of S; :: thesis: ( A = B & A is locally_connected implies B is locally_connected )
assume that
A1: A = B and
A2: A is locally_connected ; :: thesis: B is locally_connected
T | A = S | B by A1, Th4;
hence S | B is locally_connected by A2, CONNSP_2:def 6; :: according to CONNSP_2:def 6 :: thesis: verum