theorem Th67: :: MATRIX13:67

for D being non empty set
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st card P = card Q holds
( [:P,Q:] c= Indices A iff ( P c= Seg (len A) & Q c= Seg (width A) ) )