let S, T be non empty TopSpace; :: thesis: ( S,T are_homeomorphic & S is locally_connected implies T is locally_connected )
given f being Function of S,T such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def 1 :: thesis: ( not S is locally_connected or T is locally_connected )
assume A2: S is locally_connected ; :: thesis: T is locally_connected
now :: thesis: for A being non empty Subset of T
for B being Subset of T st A is open & B is_a_component_of A holds
B is open
let A be non empty Subset of T; :: thesis: for B being Subset of T st A is open & B is_a_component_of A holds
B is open
let B be Subset of T; :: thesis: ( A is open & B is_a_component_of A implies B is open )
assume ( A is open & B is_a_component_of A ) ; :: thesis: B is open
then A3: ( f " A is open & f " B is_a_component_of f " A ) by A1, Th10, TOPGRP_1:26;
rng f = [#] T by A1;
then not f " A is empty by RELAT_1:139;
then f " B is open by A2, A3, CONNSP_2:18;
hence B is open by A1, TOPGRP_1:26; :: thesis: verum
end;
hence T is locally_connected by CONNSP_2:18; :: thesis: verum