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
[x,y] in R ) holds
(SgmX R,A) /. 1 = 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
[x,y] in R ) holds
(SgmX R,A) /. 1 = 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
[x,y] in R ) holds
(SgmX R,A) /. 1 = 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
[x,y] in R ) implies (SgmX R,A) /. 1 = 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
[x,y] in R and
A4: (SgmX R,A) /. 1 <> 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;
1 <= i by A6, FINSEQ_3:27;
then A8: 1 < i by A4, A7, XXREAL_0:1;
not SgmX R,A is empty by A2, RELAT_1:60, TRIANG_1:def 2;
then A9: 1 in dom (SgmX R,A) by FINSEQ_5:6;
then A10: [((SgmX R,A) /. 1),x] in R by A2, A6, A7, A8, TRIANG_1:def 2;
(SgmX R,A) /. 1 in A by A5, A9, PARTFUN2:4;
then A11: [x,((SgmX R,A) /. 1)] 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