>>748
こんな感じ？「実対称行列の固有値は実数」

n = 2;
matrix = Table[a[i, j], {i, 1, n}, {j, 1, n}];
alist = Flatten[matrix];
expr[x_] := ( Element[Eigenvalues[x], Reals]);
ForAll[Evaluate[alist],
Element[alist, Reals] && matrix == Transpose[matrix],
expr[matrix]] // FullSimplify

n=2までしか解けなかったorz