for X being non empty TopSpace
for x being Point of X holds
( X is_locally_connected_in x iff for U1 being non empty Subset of X st U1 is open & x in U1 holds
ex x1 being Point of (X | U1) st
( x1 = x & x in Int (Component_of x1) ) )