theorem Th4: :: MATRTOP3:4

for i, n being Nat st i in Seg n holds
Det (AxialSymmetry (i,n)) = - (1. F_Real)