let a, b, c, d, e, f be Real; :: thesis: symmetric_3 (a,b,c,d,e,f) is symmetric
reconsider a = a, b = b, c = c, d = d, e = e, f = f as Element of F_Real by XREAL_0:def 1;
(symmetric_3 (a,b,c,d,e,f)) @ = <*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*> by Th05;
hence symmetric_3 (a,b,c,d,e,f) is symmetric by MATRIX_6:def 5; :: thesis: verum