theorem :: MATRIX_0:65

for D being non empty set
for G being Matrix of D
for i being Nat st width G > 1 & i in Seg (width G) holds
not DelCol (G,i) is empty-yielding