theorem :: BKMODEL1:93

for ra being non zero Real
for O, N, M being invertible Matrix of 3,F_Real st O = symmetric_3 (1,1,(- 1),0,0,0) & M = symmetric_3 (ra,ra,(- ra),0,0,0) & M = ((N @) * O) * N & (homography M) .: absolute = absolute holds
(homography N) .: absolute = absolute