theorem :: MATRIX_6:25

for n being Nat
for K being Field
for M1 being Matrix of n,K st M1 is upper_triangular Matrix of n,K & M1 is lower_triangular Matrix of n,K holds
M1 is symmetric