theorem Th28: :: MATRTOP3:28

for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Mx2Tran (Rotation (i,j,n,r)) is base_rotation