theorem Th23: :: TOPREALB:23

for p, q being Point of (Tunit_circle 2) st p <> q holds
q is Point of (Topen_unit_circle p)