let X be non empty set ; :: thesis: for A being non empty finite Subset of X
for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX R,A) /. (len (SgmX R,A)) = x
let A be non empty finite Subset of X; :: thesis: for R being Order of X
for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX R,A) /. (len (SgmX R,A)) = x
let R be Order of X; :: thesis: for x being Element of X st x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) holds
(SgmX R,A) /. (len (SgmX R,A)) = x
let x be Element of X; :: thesis: ( x in A & R linearly_orders A & ( for y being Element of X st y in A holds
[y,x] in R ) implies (SgmX R,A) /. (len (SgmX R,A)) = x )
assume that
A1: x in A and
A2: R linearly_orders A and
A3: for y being Element of X st y in A holds
[y,x] in R and
A4: (SgmX R,A) /. (len (SgmX R,A)) <> x ; :: thesis: contradiction
A5: A = rng (SgmX R,A) by A2, TRIANG_1:def 2;
then consider i being Element of NAT such that
A6: i in dom (SgmX R,A) and
A7: (SgmX R,A) /. i = x by A1, PARTFUN2:4;
set L = len (SgmX R,A);
i <= len (SgmX R,A) by A6, FINSEQ_3:27;
then A8: i < len (SgmX R,A) by A4, A7, XXREAL_0:1;
not SgmX R,A is empty by A2, RELAT_1:60, TRIANG_1:def 2;
then A9: len (SgmX R,A) in dom (SgmX R,A) by FINSEQ_5:6;
then A10: [x,((SgmX R,A) /. (len (SgmX R,A)))] in R by A2, A6, A7, A8, TRIANG_1:def 2;
(SgmX R,A) /. (len (SgmX R,A)) in A by A5, A9, PARTFUN2:4;
then A11: [((SgmX R,A) /. (len (SgmX R,A))),x] in R by A3;
field R = X by ORDERS_1:97;
then R is_antisymmetric_in X by RELAT_2:def 12;
hence contradiction by A4, A10, A11, RELAT_2:def 4; :: thesis: verum