:: deftheorem defines is_locally_connected_in CONNSP_2:def 5 :
for X being non empty TopSpace
for A being Subset of X
for x being Point of X holds
( A is_locally_connected_in x iff for B being non empty Subset of X st A = B holds
ex x1 being Point of (X | B) st
( x1 = x & X | B is_locally_connected_in x1 ) );