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
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 that
A3: A is open and
A4: B is_a_component_of A ; :: thesis: B is open
rng f = [#] T by A1, TOPS_2:def 5;
then A5: not f " A is empty by RELAT_1:174;
A6: f " A is open by A1, A3, TOPGRP_1:26;
f " B is_a_component_of f " A by A1, A4, Th10;
then f " B is open by A2, A5, A6, CONNSP_2:24;
hence B is open by A1, TOPGRP_1:26; :: thesis: verum
end;
hence T is locally_connected by CONNSP_2:24; :: thesis: verum