let a be non zero Real; :: thesis: for N being Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds
N is invertible
let N be Matrix of 3,F_Real; :: thesis: ( N = symmetric_3 (a,a,(- a),0,0,0) implies N is invertible )
assume A1: N = symmetric_3 (a,a,(- a),0,0,0) ; :: thesis: N is invertible
( (symmetric_3 (a,a,(- a),0,0,0)) * (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) = 1. (F_Real,3) & (symmetric_3 ((1 / a),(1 / a),(- (1 / a)),0,0,0)) * (symmetric_3 (a,a,(- a),0,0,0)) = 1. (F_Real,3) ) by Th41, Th42;
hence N is invertible by A1, MATRIX_6:def 2, MATRIX_6:def 3; :: thesis: verum