theorem Th84: :: JORDAN2C:100

for p, q being Point of (TOP-REAL 2)
for r being Real st p `1 = q `2 & - (p `2) = q `1 & p = r * q holds
( p `1 = 0 & p `2 = 0 & p = 0. (TOP-REAL 2) )