for K being Field
for M being Matrix of K
for P, P1, Q1 being finite without_zero Subset of NAT st card P1 = card Q1 & P c= P1 & Det (EqSegm (M,P1,Q1)) <> 0. K holds
ex Q being finite without_zero Subset of NAT st
( Q c= Q1 & card P = card Q & Det (EqSegm (M,P,Q)) <> 0. K )