set M = the Diagonal of n,K;
take the Diagonal of n,K ; :: thesis: ( the Diagonal of n,K is lower_triangular & the Diagonal of n,K is upper_triangular )
thus ( the Diagonal of n,K is lower_triangular & the Diagonal of n,K is upper_triangular ) ; :: thesis: verum