let M be Matrix of n,K; :: thesis: ( M is symmetry_circulant implies M is symmetric )
assume M is symmetry_circulant ; :: thesis: M is symmetric
hence M @ = M by Th13; :: according to MATRIX_6:def 5 :: thesis: verum