for T being non empty TopSpace
for A being Subset of T st A is open holds
for p, q being Point of T st p in A & (T_0-canonical_map T) . p = (T_0-canonical_map T) . q holds
q in A