theorem :: BKMODEL1:51

for a being non zero Real
for N being Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds
N is invertible