theorem Th6: :: T_0TOPSP:6
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