theorem :: BKMODEL1:22

for M being Matrix of 3,F_Real st M = symmetric_3 (0,0,0,0,0,0) holds
Det M = 0. F_Real