theorem :: BKMODEL4:18

for N being Matrix of 3,F_Real st N = <*<*2,0,(- 1)*>,<*0,(sqrt 3),0*>,<*1,0,(- 2)*>*> holds
( Det N = (- 3) * (sqrt 3) & N is invertible )