consider M being Diagonal of n,K;
take M ; :: thesis: ( M is lower_triangular & M is upper_triangular )
thus ( M is lower_triangular & M is upper_triangular ) ; :: thesis: verum