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; (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; verum