:: On Ordering of Bags
:: by Gilbert Lee and Piotr Rudnicki
::
:: Received March 12, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

theorem Th1: :: BAGORDER:1
for x, y, z being set st z in x & z in y & x \ {z} = y \ {z} holds
x = y
proofend;

theorem :: BAGORDER:2
for n, k being Element of NAT holds
( k in Seg n iff ( k - 1 is Element of NAT &amp; k - 1 < n ) )
proofend;

registration
let f be finite-support Function;
let X be set ;
clusterf | X ->  finite-support ;
coherence
 f | X is finite-support
proofend;
end;

theorem :: BAGORDER:3
canceled;

theorem Th4: :: BAGORDER:4
for fs being FinSequence of NAT holds
( Sum fs = 0 iff fs = (len fs) |-> 0 )
proofend;

definition
let n, i, j be Nat;
let b be ManySortedSet of n;
func(i,j) -cut b ->  ManySortedSet of j -' i means :Def1: :: BAGORDER:def 1
 for k being Element of NAT st k in j -' i holds
it . k = b . (i + k);
existence
 ex b1 being ManySortedSet of j -' i st
for k being Element of NAT st k in j -' i holds
b1 . k = b . (i + k)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of j -' i st ( for k being Element of NAT st k in j -' i holds
b1 . k = b . (i + k) ) &amp; ( for k being Element of NAT st k in j -' i holds
b2 . k = b . (i + k) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines -cut BAGORDER:def_1_:_
 for n, i, j being Nat
for b being ManySortedSet of n
for b5 being ManySortedSet of j -' i holds
( b5 = (i,j) -cut b iff for k being Element of NAT st k in j -' i holds
b5 . k = b . (i + k) );

registration
let n, i, j be Nat;
let b be natural-valued ManySortedSet of n;
cluster(i,j) -cut b ->  natural-valued ;
coherence
 (i,j) -cut b is natural-valued
proofend;
end;

registration
let n, i, j be Element of NAT ;
let b be finite-support ManySortedSet of n;
cluster(i,j) -cut b ->  finite-support ;
coherence
 (i,j) -cut b is finite-support ;
end;

theorem Th5: :: BAGORDER:5
for n, i being Nat
for a, b being ManySortedSet of n holds
( a = b iff ( (0,(i + 1)) -cut a = (0,(i + 1)) -cut b &amp; ((i + 1),n) -cut a = ((i + 1),n) -cut b ) )
proofend;

definition
let x be non empty set ;
let n be non empty Element of NAT ;
func Fin (x,n) ->  set  equals :: BAGORDER:def 2
 {  y where y is Subset of x : ( y is finite &amp; not y is empty &amp; card y c= n )  }  ;
coherence
  {  y where y is Subset of x : ( y is finite &amp; not y is empty &amp; card y c= n )  }  is set ;
end;

:: deftheorem  defines Fin BAGORDER:def_2_:_
 for x being non empty set
for n being non empty Element of NAT holds Fin (x,n) =  {  y where y is Subset of x : ( y is finite &amp; not y is empty &amp; card y c= n )  }  ;

registration
let x be non empty set ;
let n be non empty Element of NAT ;
cluster Fin (x,n) ->  non empty ;
coherence
 not Fin (x,n) is empty
proofend;
end;

theorem Th6: :: BAGORDER:6
for R being non empty transitive antisymmetric RelStr
for X being finite Subset of R st X <> {} holds
ex x being Element of R st
( x in X &amp; x is_maximal_wrt X, the InternalRel of R )
proofend;

theorem Th7: :: BAGORDER:7
for R being non empty transitive antisymmetric RelStr
for X being finite Subset of R st X <> {} holds
ex x being Element of R st
( x in X &amp; x is_minimal_wrt X, the InternalRel of R )
proofend;

theorem :: BAGORDER:8
for R being non empty transitive antisymmetric RelStr
for f being sequence of R st f is descending holds
for j, i being Nat st i < j holds
( f . i <> f . j &amp; [(f . j),(f . i)] in the InternalRel of R )
proofend;

definition
let R be non empty RelStr ;
let s be sequence of R;
attrs is non-increasing  means :Def3: :: BAGORDER:def 3
 for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R;
end;

:: deftheorem Def3 defines non-increasing BAGORDER:def_3_:_
 for R being non empty RelStr
for s being sequence of R holds
( s is non-increasing iff for i being Nat holds [(s . (i + 1)),(s . i)] in the InternalRel of R );

theorem Th9: :: BAGORDER:9
for R being non empty transitive RelStr
for f being sequence of R st f is non-increasing holds
for j, i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R
proofend;

theorem Th10: :: BAGORDER:10
for R being non empty transitive RelStr
for s being sequence of R st R is well_founded &amp; s is non-increasing holds
ex p being Nat st
for r being Nat st p <= r holds
s . p = s . r
proofend;

theorem Th11: :: BAGORDER:11
for X being set
for a being Element of X
for A being finite Subset of X
for R being Order of X st A = {a} &amp; R linearly_orders A holds
SgmX (R,A) = <*a*>
proofend;

begin

definition
let n be Ordinal;
let b be bag of n;
func TotDegree b ->  Nat means :Def4: :: BAGORDER:def 4
 ex f being FinSequence of NAT st
( it = Sum f &amp; f = b * (SgmX ((RelIncl n),(support b))) );
existence
 ex b1 being Nat ex f being FinSequence of NAT st
( b1 = Sum f &amp; f = b * (SgmX ((RelIncl n),(support b))) )
proofend;
uniqueness
 for b1, b2 being Nat st ex f being FinSequence of NAT st
( b1 = Sum f &amp; f = b * (SgmX ((RelIncl n),(support b))) ) &amp; ex f being FinSequence of NAT st
( b2 = Sum f &amp; f = b * (SgmX ((RelIncl n),(support b))) ) holds
b1 = b2 ;
end;

:: deftheorem Def4 defines TotDegree BAGORDER:def_4_:_
 for n being Ordinal
for b being bag of n
for b3 being Nat holds
( b3 = TotDegree b iff ex f being FinSequence of NAT st
( b3 = Sum f &amp; f = b * (SgmX ((RelIncl n),(support b))) ) );

theorem Th12: :: BAGORDER:12
for n being Ordinal
for b being bag of n
for s being finite Subset of n
for f, g being FinSequence of NAT st f = b * (SgmX ((RelIncl n),(support b))) &amp; g = b * (SgmX ((RelIncl n),((support b) \/ s))) holds
Sum f = Sum g
proofend;

theorem Th13: :: BAGORDER:13
for n being Ordinal
for a, b being bag of n holds TotDegree (a + b) = (TotDegree a) + (TotDegree b)
proofend;

theorem :: BAGORDER:14
for n being Ordinal
for a, b being bag of n st b divides a holds
TotDegree (a -' b) = (TotDegree a) - (TotDegree b)
proofend;

theorem Th15: :: BAGORDER:15
for n being Ordinal
for b being bag of n holds
( TotDegree b = 0 iff b = EmptyBag n )
proofend;

theorem Th16: :: BAGORDER:16
for i, j, n being Nat holds (i,j) -cut (EmptyBag n) = EmptyBag (j -' i)
proofend;

theorem Th17: :: BAGORDER:17
for i, j, n being Nat
for a, b being bag of n holds (i,j) -cut (a + b) = ((i,j) -cut a) + ((i,j) -cut b)
proofend;

theorem :: BAGORDER:18
for X being set holds support (EmptyBag X) = {}
proofend;

theorem Th19: :: BAGORDER:19
for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X
proofend;

theorem Th20: :: BAGORDER:20
for n, m being Ordinal
for b being bag of n st m in n holds
b | m is bag of m
proofend;

theorem :: BAGORDER:21
for n being Ordinal
for a, b being bag of n st b divides a holds
support b c= support a
proofend;

begin

definition
let n be set ;
mode TermOrder of n is Order of (Bags n);
end;

notation
let n be Ordinal;
synonym  LexOrder n for  BagOrder n;
end;

definition
let n be Ordinal;
let T be TermOrder of n;
attrT is admissible  means :Def5: :: BAGORDER:def 5
( T is_strongly_connected_in Bags n &amp; ( for a being bag of n holds [(EmptyBag n),a] in T ) &amp; ( for a, b, c being bag of n st [a,b] in T holds
[(a + c),(b + c)] in T ) );
end;

:: deftheorem Def5 defines admissible BAGORDER:def_5_:_
 for n being Ordinal
for T being TermOrder of n holds
( T is admissible iff ( T is_strongly_connected_in Bags n &amp; ( for a being bag of n holds [(EmptyBag n),a] in T ) &amp; ( for a, b, c being bag of n st [a,b] in T holds
[(a + c),(b + c)] in T ) ) );

theorem Th22: :: BAGORDER:22
for n being Ordinal holds LexOrder n is admissible
proofend;

registration
let n be Ordinal;
cluster Relation-like Bags n -defined Bags n -valued total V18( Bags n, Bags n) reflexive antisymmetric transitive admissible for Element of bool [:(Bags n),(Bags n):];
existence
 ex b1 being TermOrder of n st b1 is admissible
proofend;
end;

registration
let n be Ordinal;
cluster LexOrder n ->  admissible ;
coherence
 LexOrder n is admissible by Th22;
end;

theorem :: BAGORDER:23
for o being infinite Ordinal holds not LexOrder o is well-ordering
proofend;

definition
let n be Ordinal;
func InvLexOrder n ->  TermOrder of n means :Def6: :: BAGORDER:def 6
 for p, q being bag of n holds
( [p,q] in it iff ( p = q or ex i being Ordinal st
( i in n &amp; p . i < q . i &amp; ( for k being Ordinal st i in k &amp; k in n holds
p . k = q . k ) ) ) );
existence
 ex b1 being TermOrder of n st
for p, q being bag of n holds
( [p,q] in b1 iff ( p = q or ex i being Ordinal st
( i in n &amp; p . i < q . i &amp; ( for k being Ordinal st i in k &amp; k in n holds
p . k = q . k ) ) ) )
proofend;
uniqueness
 for b1, b2 being TermOrder of n st ( for p, q being bag of n holds
( [p,q] in b1 iff ( p = q or ex i being Ordinal st
( i in n &amp; p . i < q . i &amp; ( for k being Ordinal st i in k &amp; k in n holds
p . k = q . k ) ) ) ) ) &amp; ( for p, q being bag of n holds
( [p,q] in b2 iff ( p = q or ex i being Ordinal st
( i in n &amp; p . i < q . i &amp; ( for k being Ordinal st i in k &amp; k in n holds
p . k = q . k ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines InvLexOrder BAGORDER:def_6_:_
 for n being Ordinal
for b2 being TermOrder of n holds
( b2 = InvLexOrder n iff for p, q being bag of n holds
( [p,q] in b2 iff ( p = q or ex i being Ordinal st
( i in n &amp; p . i < q . i &amp; ( for k being Ordinal st i in k &amp; k in n holds
p . k = q . k ) ) ) ) );

theorem Th24: :: BAGORDER:24
for n being Ordinal holds InvLexOrder n is admissible
proofend;

registration
let n be Ordinal;
cluster InvLexOrder n ->  admissible ;
coherence
 InvLexOrder n is admissible by Th24;
end;

theorem Th25: :: BAGORDER:25
for o being Ordinal holds InvLexOrder o is well-ordering
proofend;

definition
let n be Ordinal;
let o be TermOrder of n;
assume B1: for a, b, c being bag of n st [a,b] in o holds
[(a + c),(b + c)] in o ;
func Graded o ->  TermOrder of n means :Def7: :: BAGORDER:def 7
 for a, b being bag of n holds
( [a,b] in it iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b &amp; [a,b] in o ) ) );
existence
 ex b1 being TermOrder of n st
for a, b being bag of n holds
( [a,b] in b1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b &amp; [a,b] in o ) ) )
proofend;
uniqueness
 for b1, b2 being TermOrder of n st ( for a, b being bag of n holds
( [a,b] in b1 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b &amp; [a,b] in o ) ) ) ) &amp; ( for a, b being bag of n holds
( [a,b] in b2 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b &amp; [a,b] in o ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines Graded BAGORDER:def_7_:_
 for n being Ordinal
for o being TermOrder of n st ( for a, b, c being bag of n st [a,b] in o holds
[(a + c),(b + c)] in o ) holds
for b3 being TermOrder of n holds
( b3 = Graded o iff for a, b being bag of n holds
( [a,b] in b3 iff ( TotDegree a < TotDegree b or ( TotDegree a = TotDegree b &amp; [a,b] in o ) ) ) );

theorem Th26: :: BAGORDER:26
for n being Ordinal
for o being TermOrder of n st ( for a, b, c being bag of n st [a,b] in o holds
[(a + c),(b + c)] in o ) &amp; o is_strongly_connected_in Bags n holds
Graded o is admissible
proofend;

definition
let n be Ordinal;
func GrLexOrder n ->  TermOrder of n equals :: BAGORDER:def 8
 Graded (LexOrder n);
coherence
 Graded (LexOrder n) is TermOrder of n ;
func GrInvLexOrder n ->  TermOrder of n equals :: BAGORDER:def 9
 Graded (InvLexOrder n);
coherence
 Graded (InvLexOrder n) is TermOrder of n ;
end;

:: deftheorem  defines GrLexOrder BAGORDER:def_8_:_
 for n being Ordinal holds GrLexOrder n = Graded (LexOrder n);

:: deftheorem  defines GrInvLexOrder BAGORDER:def_9_:_
 for n being Ordinal holds GrInvLexOrder n = Graded (InvLexOrder n);

theorem Th27: :: BAGORDER:27
for n being Ordinal holds GrLexOrder n is admissible
proofend;

registration
let n be Ordinal;
cluster GrLexOrder n ->  admissible ;
coherence
 GrLexOrder n is admissible by Th27;
end;

theorem :: BAGORDER:28
for o being infinite Ordinal holds not GrLexOrder o is well-ordering
proofend;

theorem Th29: :: BAGORDER:29
for n being Ordinal holds GrInvLexOrder n is admissible
proofend;

registration
let n be Ordinal;
cluster GrInvLexOrder n ->  admissible ;
coherence
 GrInvLexOrder n is admissible by Th29;
end;

theorem :: BAGORDER:30
for o being Ordinal holds GrInvLexOrder o is well-ordering
proofend;

definition
let i, n be Nat;
let o1 be TermOrder of (i + 1);
let o2 be TermOrder of (n -' (i + 1));
func BlockOrder (i,n,o1,o2) ->  TermOrder of n means :Def10: :: BAGORDER:def 10
 for p, q being bag of n holds
( [p,q] in it iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q &amp; [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q &amp; [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) );
existence
 ex b1 being TermOrder of n st
for p, q being bag of n holds
( [p,q] in b1 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q &amp; [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q &amp; [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) )
proofend;
uniqueness
 for b1, b2 being TermOrder of n st ( for p, q being bag of n holds
( [p,q] in b1 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q &amp; [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q &amp; [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) ) &amp; ( for p, q being bag of n holds
( [p,q] in b2 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q &amp; [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q &amp; [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines BlockOrder BAGORDER:def_10_:_
 for i, n being Nat
for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1))
for b5 being TermOrder of n holds
( b5 = BlockOrder (i,n,o1,o2) iff for p, q being bag of n holds
( [p,q] in b5 iff ( ( (0,(i + 1)) -cut p <> (0,(i + 1)) -cut q &amp; [((0,(i + 1)) -cut p),((0,(i + 1)) -cut q)] in o1 ) or ( (0,(i + 1)) -cut p = (0,(i + 1)) -cut q &amp; [(((i + 1),n) -cut p),(((i + 1),n) -cut q)] in o2 ) ) ) );

theorem :: BAGORDER:31
for i, n being Nat
for o1 being TermOrder of (i + 1)
for o2 being TermOrder of (n -' (i + 1)) st o1 is admissible &amp; o2 is admissible holds
BlockOrder (i,n,o1,o2) is admissible
proofend;

definition
let n be Nat;
func NaivelyOrderedBags n ->  strict RelStr  means :Def11: :: BAGORDER:def 11
( the carrier of it = Bags n &amp; ( for x, y being bag of n holds
( [x,y] in the InternalRel of it iff x divides y ) ) );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = Bags n &amp; ( for x, y being bag of n holds
( [x,y] in the InternalRel of b1 iff x divides y ) ) )
proofend;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = Bags n &amp; ( for x, y being bag of n holds
( [x,y] in the InternalRel of b1 iff x divides y ) ) &amp; the carrier of b2 = Bags n &amp; ( for x, y being bag of n holds
( [x,y] in the InternalRel of b2 iff x divides y ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines NaivelyOrderedBags BAGORDER:def_11_:_
 for n being Nat
for b2 being strict RelStr holds
( b2 = NaivelyOrderedBags n iff ( the carrier of b2 = Bags n &amp; ( for x, y being bag of n holds
( [x,y] in the InternalRel of b2 iff x divides y ) ) ) );

theorem Th32: :: BAGORDER:32
for n being Nat holds the carrier of (product (n --> OrderedNAT)) = Bags n
proofend;

theorem Th33: :: BAGORDER:33
for n being Nat holds NaivelyOrderedBags n = product (n --> OrderedNAT)
proofend;

theorem :: BAGORDER:34
for n being Nat
for o being TermOrder of n st o is admissible holds
( the InternalRel of (NaivelyOrderedBags n) c= o &amp; o is well-ordering )
proofend;

begin

definition
let R be non empty connected Poset;
let X be Element of Fin the carrier of R;
assume B1: not X is empty ;
func PosetMin X ->  Element of R means :: BAGORDER:def 12
( it in X &amp; it is_minimal_wrt X, the InternalRel of R );
existence
 ex b1 being Element of R st
( b1 in X &amp; b1 is_minimal_wrt X, the InternalRel of R )
proofend;
uniqueness
 for b1, b2 being Element of R st b1 in X &amp; b1 is_minimal_wrt X, the InternalRel of R &amp; b2 in X &amp; b2 is_minimal_wrt X, the InternalRel of R holds
b1 = b2
proofend;
func PosetMax X ->  Element of R means :Def13: :: BAGORDER:def 13
( it in X &amp; it is_maximal_wrt X, the InternalRel of R );
existence
 ex b1 being Element of R st
( b1 in X &amp; b1 is_maximal_wrt X, the InternalRel of R )
proofend;
uniqueness
 for b1, b2 being Element of R st b1 in X &amp; b1 is_maximal_wrt X, the InternalRel of R &amp; b2 in X &amp; b2 is_maximal_wrt X, the InternalRel of R holds
b1 = b2
proofend;
end;

:: deftheorem  defines PosetMin BAGORDER:def_12_:_
 for R being non empty connected Poset
for X being Element of Fin the carrier of R st not X is empty holds
for b3 being Element of R holds
( b3 = PosetMin X iff ( b3 in X &amp; b3 is_minimal_wrt X, the InternalRel of R ) );

:: deftheorem Def13 defines PosetMax BAGORDER:def_13_:_
 for R being non empty connected Poset
for X being Element of Fin the carrier of R st not X is empty holds
for b3 being Element of R holds
( b3 = PosetMax X iff ( b3 in X &amp; b3 is_maximal_wrt X, the InternalRel of R ) );

definition
let R be non empty connected Poset;
func FinOrd-Approx R ->  Function of NAT,(bool [:(Fin the carrier of R),(Fin the carrier of R):]) means :Def14: :: BAGORDER:def 14
( dom it = NAT &amp; it . 0 =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) )  }  &amp; ( for n being Nat holds it . (n + 1) =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in it . n )  }  ) );
existence
 ex b1 being Function of NAT,(bool [:(Fin the carrier of R),(Fin the carrier of R):]) st
( dom b1 = NAT &amp; b1 . 0 =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) )  }  &amp; ( for n being Nat holds b1 . (n + 1) =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b1 . n )  }  ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(bool [:(Fin the carrier of R),(Fin the carrier of R):]) st dom b1 = NAT &amp; b1 . 0 =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) )  }  &amp; ( for n being Nat holds b1 . (n + 1) =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b1 . n )  }  ) &amp; dom b2 = NAT &amp; b2 . 0 =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) )  }  &amp; ( for n being Nat holds b2 . (n + 1) =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b2 . n )  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines FinOrd-Approx BAGORDER:def_14_:_
 for R being non empty connected Poset
for b2 being Function of NAT,(bool [:(Fin the carrier of R),(Fin the carrier of R):]) holds
( b2 = FinOrd-Approx R iff ( dom b2 = NAT &amp; b2 . 0 =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) )  }  &amp; ( for n being Nat holds b2 . (n + 1) =  {  [x,y] where x, y is Element of Fin the carrier of R : ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in b2 . n )  }  ) ) );

theorem Th35: :: BAGORDER:35
for R being non empty connected Poset
for x, y being Element of Fin the carrier of R holds
( [x,y] in union (rng (FinOrd-Approx R)) iff ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in union (rng (FinOrd-Approx R)) ) ) )
proofend;

theorem Th36: :: BAGORDER:36
for R being non empty connected Poset
for x being Element of Fin the carrier of R st x <> {} holds
not [x,{}] in union (rng (FinOrd-Approx R))
proofend;

theorem Th37: :: BAGORDER:37
for R being non empty connected Poset
for a being Element of Fin the carrier of R holds a \ {(PosetMax a)} is Element of Fin the carrier of R
proofend;

Lm1:  for R being non empty connected Poset
for n being Nat
for a being Element of Fin the carrier of R st card a = n + 1 holds
card (a \ {(PosetMax a)}) = n
proofend;

theorem Th38: :: BAGORDER:38
for R being non empty connected Poset holds union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R)
proofend;

definition
let R be non empty connected Poset;
func FinOrd R ->  Order of (Fin the carrier of R) equals :: BAGORDER:def 15
 union (rng (FinOrd-Approx R));
coherence
 union (rng (FinOrd-Approx R)) is Order of (Fin the carrier of R) by Th38;
end;

:: deftheorem  defines FinOrd BAGORDER:def_15_:_
 for R being non empty connected Poset holds FinOrd R = union (rng (FinOrd-Approx R));

definition
let R be non empty connected Poset;
func FinPoset R ->  Poset equals :: BAGORDER:def 16
 RelStr(# (Fin the carrier of R),(FinOrd R) #);
correctness
coherence
RelStr(# (Fin the carrier of R),(FinOrd R) #) is Poset;
;
end;

:: deftheorem  defines FinPoset BAGORDER:def_16_:_
 for R being non empty connected Poset holds FinPoset R = RelStr(# (Fin the carrier of R),(FinOrd R) #);

registration
let R be non empty connected Poset;
cluster FinPoset R ->  non empty ;
correctness
coherence
not FinPoset R is empty ;
;
end;

theorem Th39: :: BAGORDER:39
for R being non empty connected Poset
for a, b being Element of (FinPoset R) holds
( [a,b] in the InternalRel of (FinPoset R) iff ex x, y being Element of Fin the carrier of R st
( a = x &amp; b = y &amp; ( x = {} or ( x <> {} &amp; y <> {} &amp; PosetMax x <> PosetMax y &amp; [(PosetMax x),(PosetMax y)] in the InternalRel of R ) or ( x <> {} &amp; y <> {} &amp; PosetMax x = PosetMax y &amp; [(x \ {(PosetMax x)}),(y \ {(PosetMax y)})] in FinOrd R ) ) ) )
proofend;

registration
let R be non empty connected Poset;
cluster FinPoset R ->  connected ;
correctness
coherence
FinPoset R is connected ;
proofend;
end;

definition
let R be non empty connected RelStr ;
let C be non empty set ;
assume that
B1: R is well_founded and
B2: C c= the carrier of R ;
func MinElement (C,R) ->  Element of R means :Def17: :: BAGORDER:def 17
( it in C &amp; it is_minimal_wrt C, the InternalRel of R );
existence
 ex b1 being Element of R st
( b1 in C &amp; b1 is_minimal_wrt C, the InternalRel of R )
proofend;
uniqueness
 for b1, b2 being Element of R st b1 in C &amp; b1 is_minimal_wrt C, the InternalRel of R &amp; b2 in C &amp; b2 is_minimal_wrt C, the InternalRel of R holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines MinElement BAGORDER:def_17_:_
 for R being non empty connected RelStr
for C being non empty set st R is well_founded &amp; C c= the carrier of R holds
for b3 being Element of R holds
( b3 = MinElement (C,R) iff ( b3 in C &amp; b3 is_minimal_wrt C, the InternalRel of R ) );

theorem Th40: :: BAGORDER:40
for R being non empty RelStr
for s being sequence of R
for j being Nat st s is descending holds
s ^\ j is descending
proofend;

theorem :: BAGORDER:41
for R being non empty connected Poset st R is well_founded holds
FinPoset R is well_founded
proofend;