defpred S₁[ Nat] means ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card Q = $1 & Det (EqSegm M,P,Q) <> 0. K );
A1: for k being Nat st S₁[k] holds
k <= len M

proof

let k be Nat; :: thesis:
assume S₁[k] ; :: thesis:
then consider P, Q being finite without_zero Subset of NAT such that
A2: ( [:P,Q:] c= Indices M & card P = card Q & card Q = k ) and
Det (EqSegm M,P,Q) <> 0. K ;
( P c= Seg (len M) & card (Seg (len M)) = len M ) by A2, Th67, FINSEQ_1:78;
hence k <= len M by A2, NAT_1:44; :: thesis:

end;

A3: ex k being Nat st S₁[k]

proof

consider E being empty finite without_zero Subset of NAT ;
reconsider E = E as finite without_zero Subset of NAT ;
take C = card E; :: thesis:
take P = E; :: thesis:
take Q = E; :: thesis:
( Det (EqSegm M,E,E) = 1_ K & E c= Seg (len M) & E c= Seg (width M) ) by CARD_1:47, MATRIXR2:41, XBOOLE_1:2;
hence ( [:P,Q:] c= Indices M & card P = card Q & card Q = C & Det (EqSegm M,P,Q) <> 0. K ) by Th67; :: thesis:

end;

consider k being Nat such that
A4: S₁[k] and
A5: for n being Nat st S₁[n] holds
n <= k from NAT_1:sch 6(A1, A3);
take k ; :: thesis:
thus ( k is Element of NAT & ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = k & Det (EqSegm M,P,Q) <> 0. K ) & ( for P1, Q1 being finite without_zero Subset of NAT st [:P1,Q1:] c= Indices M & card P1 = card Q1 & Det (EqSegm M,P1,Q1) <> 0. K holds
card P1 <= k ) ) by A4, A5; :: thesis: