theorem Th07: :: PASCAL:7

for M, N being Matrix of 3,F_Real st N is symmetric holds
((M @) * N) * M is symmetric