theorem Th27: :: MATRTOP3:27

for i, n being Nat st i in Seg n holds
Mx2Tran (AxialSymmetry (i,n)) is rotation