theorem Th20: :: MATRTOP3:20

for r being Real
for i, j, k, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k <> i & k <> j holds
((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k