for N being invertible Matrix of 3,F_Real
for NR, M1, M2 being Matrix of 3,REAL
for a, b, c, d, e, f being Real st NR = MXF2MXR N & M1 = symmetric_3 (a,b,c,(d / 2),(f / 2),(e / 2)) & M2 = ((MXF2MXR ((MXR2MXF (NR @)) ~)) * M1) * (MXF2MXR ((MXR2MXF NR) ~)) holds
MXR2MXF M2 is symmetric