theorem Th43: :: BKMODEL1:50
(symmetric_3 (1,1,(- 1),0,0,0)) * (symmetric_3 (1,1,(- 1),0,0,0)) = 1. (F_Real,3)