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, Def2;
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:2;
not SgmX (R,A) is empty by A2, Def2, RELAT_1:38;
then A8: 1 in dom (SgmX (R,A)) by FINSEQ_5:6;
then A9: [x,((SgmX (R,A)) /. 1)] in R by A3, A5, PARTFUN2:2;
A10: field R = X by ORDERS_1:12;
1 <= i by A6, FINSEQ_3:25;
then 1 < i by A4, A7, XXREAL_0:1;
then [((SgmX (R,A)) /. 1),x] in R by A2, A6, A7, A8, Def2;
hence contradiction by A4, A9, A10, RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum