theorem Th45: :: BORSUK_7:55

for s being Real
for p being Point of (TOP-REAL 2) st (Rotate s) . p = 0. (TOP-REAL 2) holds
p = 0. (TOP-REAL 2)