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
A11: 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
A12: 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
A13: 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
A14: 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
A15: n2 <= n1 by A12, A13;
n1 <= n2 by A11, A14;
hence n1 = n2 by A15, XXREAL_0:1; :: thesis: verum