let n1, n2 be Element of NAT ; :: thesis: ( ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = n1 & 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 <= n1 ) & ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = n2 & 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 <= n2 ) implies n1 = n2 )
assume that
A6: ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = n1 & Det (EqSegm M,P,Q) <> 0. K ) and
A7: 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 <= n1 and
A8: ex P, Q being finite without_zero Subset of NAT st
( [:P,Q:] c= Indices M & card P = card Q & card P = n2 & Det (EqSegm M,P,Q) <> 0. K ) and
A9: 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 <= n2 ; :: thesis: n1 = n2
( n1 <= n2 & n2 <= n1 ) by A6, A7, A8, A9;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum