let M be Diagonal of n,K; :: thesis: ( M is upper_triangular & M is lower_triangular )
for i, j being Nat st [i,j] in Indices M & i > j holds
M * (i,j) = 0. K by MATRIX_1:def 14;
hence M is upper_triangular by Def3; :: thesis: M is lower_triangular
thus for i, j being Nat st [i,j] in Indices M & i < j holds
M * (i,j) = 0. K by MATRIX_1:def 14; :: according to MATRIX_2:def 4 :: thesis: verum