A1: symmetric_3 (1,1,(- 1),0,0,0) is_reverse_of symmetric_3 (1,1,(- 1),0,0,0) by Th43, MATRIX_6:def 2;
thus symmetric_3 (1,1,(- 1),0,0,0) is invertible Matrix of 3,F_Real by Th43, MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: (symmetric_3 (1,1,(- 1),0,0,0)) ~ = symmetric_3 (1,1,(- 1),0,0,0)
hence (symmetric_3 (1,1,(- 1),0,0,0)) ~ = symmetric_3 (1,1,(- 1),0,0,0) by A1, MATRIX_6:def 4; :: thesis: verum