for ra being Real
for M, N being Matrix of 3,F_Real
for MR, NR being Matrix of 3,REAL st MR = M & NR = N & N is symmetric & MR = ra * NR holds
M is symmetric