:: deftheorem defines is_locally_connected_in CONNSP_2:def 3 :
for X being non empty TopSpace
for x being Point of X holds
( X is_locally_connected_in x iff for U1 being Subset of X st U1 is a_neighborhood of x holds
ex V being Subset of X st
( V is a_neighborhood of x & V is connected & V c= U1 ) );