reconsider fr1 = a, fr2 = b, fr3 = c, fr4 = d, fr5 = e, fr6 = f as Element of F_Real by XREAL_0:def 1;
set S = <*<*fr1,fr4,fr5*>,<*fr4,fr2,fr6*>,<*fr5,fr6,fr3*>*>;
<*<*fr1,fr4,fr5*>,<*fr4,fr2,fr6*>,<*fr5,fr6,fr3*>*> is Matrix of 3,F_Real by MATRIXR2:35;
hence <*<*a,d,e*>,<*d,b,f*>,<*e,f,c*>*> is Matrix of 3,F_Real ; :: thesis: verum