theorem Th44: :: BKMODEL1:52

( symmetric_3 (1,1,(- 1),0,0,0) is invertible Matrix of 3,F_Real & (symmetric_3 (1,1,(- 1),0,0,0)) ~ = symmetric_3 (1,1,(- 1),0,0,0) )