theorem Th24: :: MATRTOP3:24

for s being Real
for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds
ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s