orders_2.miz



    begin

    reserve X,Y,x,y for set;

    definition

      struct ( 1-sorted) RelStr (# the carrier -> set,

the InternalRel -> Relation of the carrier #)

       attr strict strict;

    end

    registration

      let X be non empty set;

      let R be Relation of X;

      cluster RelStr (# X, R #) -> non empty;

      coherence ;

    end

    definition

      let A be RelStr;

      :: ORDERS_2:def1

      attr A is total means

      : Def1: the InternalRel of A is total;

      :: ORDERS_2:def2

      attr A is reflexive means

      : Def2: the InternalRel of A is_reflexive_in the carrier of A;

      :: ORDERS_2:def3

      attr A is transitive means

      : Def3: the InternalRel of A is_transitive_in the carrier of A;

      :: ORDERS_2:def4

      attr A is antisymmetric means

      : Def4: the InternalRel of A is_antisymmetric_in the carrier of A;

    end

    registration

      cluster reflexive transitive antisymmetric strict total1 -element for RelStr;

      existence

      proof

        set R = the Order of { {} };

        take L = RelStr (# { {} }, R #);

        

         A1: ( field R) = the carrier of L by ORDERS_1: 12;

        hence the InternalRel of L is_reflexive_in the carrier of L by RELAT_2:def 9;

        thus the InternalRel of L is_transitive_in the carrier of L by A1, RELAT_2:def 16;

        thus the InternalRel of L is_antisymmetric_in the carrier of L by A1, RELAT_2:def 12;

        thus L is strict;

        thus the InternalRel of L is total;

        thus the carrier of L is 1 -element;

      end;

    end

    registration

      cluster reflexive -> total for RelStr;

      coherence

      proof

        let L be RelStr;

        assume L is reflexive;

        then the InternalRel of L is_reflexive_in the carrier of L;

        then ( dom the InternalRel of L) = the carrier of L by ORDERS_1: 13;

        hence the InternalRel of L is total by PARTFUN1:def 2;

      end;

    end

    definition

      mode Poset is reflexive transitive antisymmetric RelStr;

    end

    registration

      let A be total RelStr;

      cluster the InternalRel of A -> total;

      coherence by Def1;

    end

    registration

      let A be reflexive RelStr;

      cluster the InternalRel of A -> reflexive;

      coherence

      proof

        set R = the InternalRel of A;

        R is_reflexive_in the carrier of A by Def2;

        then

         A1: ( field R) = the carrier of A by ORDERS_1: 13;

        the InternalRel of A is_reflexive_in the carrier of A by Def2;

        hence thesis by A1;

      end;

    end

    registration

      let A be total antisymmetric RelStr;

      cluster the InternalRel of A -> antisymmetric;

      coherence

      proof

        set R = the InternalRel of A;

        ( field R) = the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A by Def4, ORDERS_1: 12;

        hence thesis;

      end;

    end

    registration

      let A be transitive RelStr;

      cluster the InternalRel of A -> transitive;

      coherence

      proof

        let a,b,c be object;

        assume

         A1: a in ( field the InternalRel of A) & b in ( field the InternalRel of A) & c in ( field the InternalRel of A);

        ( field the InternalRel of A) c= (the carrier of A \/ the carrier of A) by RELSET_1: 8;

        hence thesis by A1, RELAT_2:def 8, Def3;

      end;

    end

    registration

      let X be set;

      let O be total reflexive Relation of X;

      cluster RelStr (# X, O #) -> reflexive;

      coherence

      proof

        set A = RelStr (# X, O #);

        ( field O) = X by ORDERS_1: 12;

        hence the InternalRel of A is_reflexive_in the carrier of A by RELAT_2:def 9;

      end;

    end

    registration

      let X be set;

      let O be total transitive Relation of X;

      cluster RelStr (# X, O #) -> transitive;

      coherence

      proof

        set A = RelStr (# X, O #);

        ( field O) = X by ORDERS_1: 12;

        hence the InternalRel of A is_transitive_in the carrier of A by RELAT_2:def 16;

      end;

    end

    registration

      let X be set;

      let O be total antisymmetric Relation of X;

      cluster RelStr (# X, O #) -> antisymmetric;

      coherence

      proof

        set A = RelStr (# X, O #);

        ( field O) = X by ORDERS_1: 12;

        hence the InternalRel of A is_antisymmetric_in the carrier of A by RELAT_2:def 12;

      end;

    end

    reserve A for non empty Poset;

    reserve a,a1,a2,a3,b,c for Element of A;

    reserve S,T for Subset of A;

    

     Lm1: x in S implies x is Element of A;

    definition

      let A be RelStr;

      let a1,a2 be Element of A;

      :: ORDERS_2:def5

      pred a1 <= a2 means [a1, a2] in the InternalRel of A;

    end

    notation

      let A be RelStr;

      let a1,a2 be Element of A;

      synonym a2 >= a1 for a1 <= a2;

    end

    definition

      let A be RelStr;

      let a1,a2 be Element of A;

      :: ORDERS_2:def6

      pred a1 < a2 means a1 <= a2 & a1 <> a2;

      irreflexivity ;

    end

    notation

      let A be RelStr;

      let a1,a2 be Element of A;

      synonym a2 > a1 for a1 < a2;

    end

    theorem :: ORDERS_2:1

    

     Th1: for A be reflexive non empty RelStr, a be Element of A holds a <= a

    proof

      let A be reflexive non empty RelStr, a be Element of A;

      the InternalRel of A is_reflexive_in the carrier of A by Def2;

      then [a, a] in the InternalRel of A;

      hence thesis;

    end;

    definition

      let A be reflexive non empty RelStr;

      let a1,a2 be Element of A;

      :: original: <=

      redefine

      pred a1 <= a2;

      reflexivity by Th1;

    end

    theorem :: ORDERS_2:2

    

     Th2: for A be antisymmetric RelStr, a1,a2 be Element of A st a1 <= a2 & a2 <= a1 holds a1 = a2

    proof

      let A be antisymmetric RelStr, a1,a2 be Element of A;

      assume that

       A1: [a1, a2] in the InternalRel of A and

       A2: [a2, a1] in the InternalRel of A;

      

       A3: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;

      a1 in the carrier of A by A1, ZFMISC_1: 87;

      hence thesis by A1, A2, A3;

    end;

    theorem :: ORDERS_2:3

    

     Th3: for A be transitive RelStr, a1,a2,a3 be Element of A holds a1 <= a2 & a2 <= a3 implies a1 <= a3

    proof

      let A be transitive RelStr, a1,a2,a3 be Element of A;

      assume that

       A1: [a1, a2] in the InternalRel of A and

       A2: [a2, a3] in the InternalRel of A;

      

       A3: the InternalRel of A is_transitive_in the carrier of A by Def3;

      a1 in the carrier of A by A1, ZFMISC_1: 87;

      hence [a1, a3] in the InternalRel of A by A1, A2, A3;

    end;

    theorem :: ORDERS_2:4

    

     Th4: for A be antisymmetric RelStr, a1,a2 be Element of A holds not (a1 < a2 & a2 < a1) by Th2;

    theorem :: ORDERS_2:5

    

     Th5: for A be transitive antisymmetric RelStr holds for a1,a2,a3 be Element of A holds a1 < a2 & a2 < a3 implies a1 < a3 by Th3, Th4;

    theorem :: ORDERS_2:6

    

     Th6: for A be antisymmetric RelStr, a1,a2 be Element of A holds a1 <= a2 implies not a2 < a1 by Th2;

    theorem :: ORDERS_2:7

    

     Th7: for A be transitive antisymmetric RelStr holds for a1,a2,a3 be Element of A holds a1 < a2 & a2 <= a3 or a1 <= a2 & a2 < a3 implies a1 < a3 by Th2, Th3;

    definition

      let A be RelStr;

      let IT be Subset of A;

      :: ORDERS_2:def7

      attr IT is strongly_connected means

      : Def7: the InternalRel of A is_strongly_connected_in IT;

    end

    registration

      let A be RelStr;

      cluster empty -> strongly_connected for Subset of A;

      coherence

      proof

        let S be Subset of A;

        assume S is empty;

        then

         A1: S = ( {} A);

        let x1,x2 be object;

        thus thesis by A1;

      end;

    end

    registration

      let A be RelStr;

      cluster strongly_connected for Subset of A;

      existence

      proof

        take ( {} A);

        thus thesis;

      end;

    end

    definition

      let A be RelStr;

      mode Chain of A is strongly_connected Subset of A;

    end

    theorem :: ORDERS_2:8

    

     Th8: for A be non empty reflexive RelStr holds for a be Element of A holds {a} is Chain of A

    proof

      let A be non empty reflexive RelStr, a be Element of A;

      

       A1: the InternalRel of A is_reflexive_in the carrier of A by Def2;

       {a} is strongly_connected

      proof

        let x1,x2 be object;

        assume x1 in {a} & x2 in {a};

        then x1 = a & x2 = a by TARSKI:def 1;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: ORDERS_2:9

    

     Th9: for A be non empty reflexive RelStr, a1,a2 be Element of A holds {a1, a2} is Chain of A iff a1 <= a2 or a2 <= a1

    proof

      let A be non empty reflexive RelStr, a1,a2 be Element of A;

      

       A1: a2 <= a2;

      thus {a1, a2} is Chain of A implies a1 <= a2 or a2 <= a1

      proof

        assume {a1, a2} is Chain of A;

        then

         A2: the InternalRel of A is_strongly_connected_in {a1, a2} by Def7;

        a1 in {a1, a2} & a2 in {a1, a2} by TARSKI:def 2;

        then [a1, a2] in the InternalRel of A or [a2, a1] in the InternalRel of A by A2;

        hence thesis;

      end;

      assume

       A3: a1 <= a2 or a2 <= a1;

      

       A4: a1 <= a1;

       {a1, a2} is strongly_connected

      proof

        let x,y be object;

        assume

         A5: x in {a1, a2} & y in {a1, a2};

        now

          per cases by A5, TARSKI:def 2;

            suppose x = a1 & y = a1;

            hence thesis by A4;

          end;

            suppose x = a1 & y = a2;

            hence thesis by A3;

          end;

            suppose x = a2 & y = a1;

            hence thesis by A3;

          end;

            suppose x = a2 & y = a2;

            hence thesis by A1;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ORDERS_2:10

    for A be RelStr, C be Chain of A, S be Subset of A holds S c= C implies S is Chain of A

    proof

      let A be RelStr, C be Chain of A, S be Subset of A;

      assume

       A1: S c= C;

      the InternalRel of A is_strongly_connected_in C by Def7;

      then the InternalRel of A is_strongly_connected_in S by A1;

      hence thesis by Def7;

    end;

    theorem :: ORDERS_2:11

    

     Th11: for A be reflexive RelStr, a1,a2 be Element of A holds (ex C be Chain of A st a1 in C & a2 in C) iff a1 <= a2 or a2 <= a1

    proof

      let A be reflexive RelStr;

      let a1,a2 be Element of A;

      thus (ex C be Chain of A st a1 in C & a2 in C) implies a1 <= a2 or a2 <= a1

      proof

        given C be Chain of A such that

         A1: a1 in C & a2 in C;

        the InternalRel of A is_strongly_connected_in C by Def7;

        then [a1, a2] in the InternalRel of A or [a2, a1] in the InternalRel of A by A1;

        hence thesis;

      end;

      assume

       A2: a1 <= a2 or a2 <= a1;

      then [a1, a2] in the InternalRel of A or [a2, a1] in the InternalRel of A;

      then

      reconsider B = A as non empty reflexive RelStr;

      reconsider b1 = a1, b2 = a2 as Element of B;

      reconsider Y = {b1, b2} as Chain of A by A2, Th9;

      take Y;

      thus thesis by TARSKI:def 2;

    end;

    theorem :: ORDERS_2:12

    

     Th12: for A be reflexive antisymmetric RelStr, a1,a2 be Element of A holds (ex C be Chain of A st a1 in C & a2 in C) iff (a1 < a2 iff not a2 <= a1) by Th6, Th11;

    theorem :: ORDERS_2:13

    

     Th13: for A be RelStr, T be Subset of A holds the InternalRel of A well_orders T implies T is Chain of A by ORDERS_1: 7, Def7;

    definition

      let A;

      let S;

      :: ORDERS_2:def8

      func UpperCone (S) -> Subset of A equals { a1 : for a2 st a2 in S holds a2 < a1 };

      coherence

      proof

        set T = { a1 : for a2 st a2 in S holds a2 < a1 };

        T c= the carrier of A

        proof

          let x be object;

          assume x in T;

          then ex a1 st x = a1 & for a2 st a2 in S holds a2 < a1;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let A;

      let S;

      :: ORDERS_2:def9

      func LowerCone (S) -> Subset of A equals { a1 : for a2 st a2 in S holds a1 < a2 };

      coherence

      proof

        set T = { a1 : for a2 st a2 in S holds a1 < a2 };

        T c= the carrier of A

        proof

          let x be object;

          assume x in T;

          then ex a1 st x = a1 & for a2 st a2 in S holds a1 < a2;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ORDERS_2:14

    

     Th14: ( UpperCone ( {} A)) = the carrier of A

    proof

      thus ( UpperCone ( {} A)) c= the carrier of A;

      let x be object;

      assume x in the carrier of A;

      then

      reconsider a = x as Element of A;

      for a2 st a2 in ( {} A) holds a2 < a;

      hence thesis;

    end;

    theorem :: ORDERS_2:15

    ( UpperCone ( [#] A)) = {}

    proof

      thus ( UpperCone ( [#] A)) c= {}

      proof

        let x be object;

        assume x in ( UpperCone ( [#] A));

        then ex a st x = a & for a2 st a2 in ( [#] A) holds a2 < a;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: ORDERS_2:16

    ( LowerCone ( {} A)) = the carrier of A

    proof

      thus ( LowerCone ( {} A)) c= the carrier of A;

      let x be object;

      assume x in the carrier of A;

      then

      reconsider a = x as Element of A;

      for a2 st a2 in ( {} A) holds a < a2;

      hence thesis;

    end;

    theorem :: ORDERS_2:17

    ( LowerCone ( [#] A)) = {}

    proof

      thus ( LowerCone ( [#] A)) c= {}

      proof

        let x be object;

        assume x in ( LowerCone ( [#] A));

        then ex a st x = a & for a2 st a2 in ( [#] A) holds a < a2;

        hence thesis;

      end;

      thus thesis;

    end;

    theorem :: ORDERS_2:18

    

     Th18: a in S implies not a in ( UpperCone S)

    proof

      assume that

       A1: a in S and

       A2: a in ( UpperCone S);

      ex a1 st a1 = a & for a2 st a2 in S holds a2 < a1 by A2;

      hence thesis by A1;

    end;

    theorem :: ORDERS_2:19

     not a in ( UpperCone {a})

    proof

      a in {a} by TARSKI:def 1;

      hence thesis by Th18;

    end;

    theorem :: ORDERS_2:20

    

     Th20: a in S implies not a in ( LowerCone S)

    proof

      assume that

       A1: a in S and

       A2: a in ( LowerCone S);

      ex a1 st a1 = a & for a2 st a2 in S holds a1 < a2 by A2;

      hence thesis by A1;

    end;

    theorem :: ORDERS_2:21

    

     Th21: not a in ( LowerCone {a})

    proof

      a in {a} by TARSKI:def 1;

      hence thesis by Th20;

    end;

    theorem :: ORDERS_2:22

    c < a iff a in ( UpperCone {c})

    proof

      thus c < a implies a in ( UpperCone {c})

      proof

        assume c < a;

        then for b holds b in {c} implies b < a by TARSKI:def 1;

        hence thesis;

      end;

      assume a in ( UpperCone {c});

      then

       A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a2 < a1;

      c in {c} by TARSKI:def 1;

      hence thesis by A1;

    end;

    theorem :: ORDERS_2:23

    

     Th23: a < c iff a in ( LowerCone {c})

    proof

      thus a < c implies a in ( LowerCone {c})

      proof

        assume a < c;

        then for b holds b in {c} implies a < b by TARSKI:def 1;

        hence thesis;

      end;

      assume a in ( LowerCone {c});

      then

       A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a1 < a2;

      c in {c} by TARSKI:def 1;

      hence thesis by A1;

    end;

    definition

      let A;

      let S;

      let a;

      :: ORDERS_2:def10

      func InitSegm (S,a) -> Subset of A equals (( LowerCone {a}) /\ S);

      correctness ;

    end

    definition

      let A;

      let S;

      :: ORDERS_2:def11

      mode Initial_Segm of S -> Subset of A means

      : Def11: ex a st a in S & it = ( InitSegm (S,a)) if S <> {}

      otherwise it = {} ;

      existence

      proof

        now

          set x = the Element of S;

          assume S <> {} ;

          then

          reconsider x as Element of A by Lm1;

          take T = ( InitSegm (S,x));

          thus S <> {} implies ex a st a in S & T = ( InitSegm (S,a));

          thus S = {} implies T = {} ;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: ORDERS_2:24

    

     Th24: a in ( InitSegm (S,b)) iff a < b & a in S

    proof

      a in ( InitSegm (S,b)) iff a in ( LowerCone {b}) & a in S by XBOOLE_0:def 4;

      hence thesis by Th23;

    end;

    theorem :: ORDERS_2:25

    ( InitSegm (( {} A),a)) = {} ;

    theorem :: ORDERS_2:26

    

     Th26: not a in ( InitSegm (S,a))

    proof

      assume not thesis;

      then a in ( LowerCone {a}) by XBOOLE_0:def 4;

      then

       A1: ex a1 st a = a1 & for a2 st a2 in {a} holds a1 < a2;

      a in {a} by TARSKI:def 1;

      hence thesis by A1;

    end;

    theorem :: ORDERS_2:27

    a1 < a2 implies ( InitSegm (S,a1)) c= ( InitSegm (S,a2))

    proof

      assume

       A1: a1 < a2;

      let x be object;

      assume

       A2: x in ( InitSegm (S,a1));

      then x in ( LowerCone {a1}) by XBOOLE_0:def 4;

      then

      consider a such that

       A3: a = x and

       A4: for b st b in {a1} holds a < b;

      a1 in {a1} by TARSKI:def 1;

      then a < a1 by A4;

      then a < a2 by A1, Th5;

      then for b holds b in {a2} implies a < b by TARSKI:def 1;

      then

       A5: x in ( LowerCone {a2}) by A3;

      x in S by A2, XBOOLE_0:def 4;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: ORDERS_2:28

    

     Th28: S c= T implies ( InitSegm (S,a)) c= ( InitSegm (T,a))

    proof

      assume

       A1: S c= T;

      let x be object;

      assume x in ( InitSegm (S,a));

      then x in S & x in ( LowerCone {a}) by XBOOLE_0:def 4;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: ORDERS_2:29

    

     Th29: for I be Initial_Segm of S holds I c= S

    proof

      let I be Initial_Segm of S;

      per cases ;

        suppose S = {} ;

        hence thesis by Def11;

      end;

        suppose S <> {} ;

        then ex a st a in S & I = ( InitSegm (S,a)) by Def11;

        hence thesis by XBOOLE_1: 17;

      end;

    end;

    theorem :: ORDERS_2:30

    

     Th30: S <> {} iff not S is Initial_Segm of S

    proof

      thus S <> {} implies not S is Initial_Segm of S

      proof

        assume S <> {} & S is Initial_Segm of S;

        then

        consider a such that

         A1: a in S & S = ( InitSegm (S,a)) by Def11;

        a in ( LowerCone {a}) by A1, XBOOLE_0:def 4;

        hence thesis by Th21;

      end;

      thus thesis by Def11;

    end;

    theorem :: ORDERS_2:31

    

     Th31: S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S

    proof

      assume that

       A1: S <> {} and

       A2: S is Initial_Segm of T and

       A3: T is Initial_Segm of S;

      now

        per cases ;

          suppose S = {} ;

          hence thesis by A1;

        end;

          suppose T = {} ;

          hence thesis by A1, A2, Def11;

        end;

          suppose

           A4: S <> {} & T <> {} ;

          then

          consider a2 such that

           A5: a2 in T and

           A6: S = ( InitSegm (T,a2)) by A2, Def11;

          consider a1 such that

           A7: a1 in S and

           A8: T = ( InitSegm (S,a1)) by A3, A4, Def11;

          a1 in ( LowerCone {a2}) by A7, A6, XBOOLE_0:def 4;

          then

           A9: ex a st a = a1 & for b st b in {a2} holds a < b;

          a2 in ( LowerCone {a1}) by A8, A5, XBOOLE_0:def 4;

          then

           A10: ex a3 st a3 = a2 & for b st b in {a1} holds a3 < b;

          a1 in {a1} by TARSKI:def 1;

          then

           A11: a2 < a1 by A10;

          a2 in {a2} by TARSKI:def 1;

          then a1 < a2 by A9;

          hence thesis by A11, Th4;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDERS_2:32

    

     Th32: a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T

    proof

      assume that

       A1: a1 < a2 and

       A2: a1 in S and

       A3: a2 in T and

       A4: T is Initial_Segm of S;

      consider a such that a in S and

       A5: T = ( InitSegm (S,a)) by A2, A4, Def11;

      now

        let b;

        assume b in {a};

        then

         A6: b = a by TARSKI:def 1;

        a2 in ( LowerCone {a}) by A3, A5, XBOOLE_0:def 4;

        then

         A7: ex a3 st a3 = a2 & for c st c in {a} holds a3 < c;

        a in {a} by TARSKI:def 1;

        then a2 < a by A7;

        hence a1 < b by A1, A6, Th5;

      end;

      then a1 in ( LowerCone {a});

      hence thesis by A2, A5, XBOOLE_0:def 4;

    end;

    theorem :: ORDERS_2:33

    

     Th33: a in S & S is Initial_Segm of T implies ( InitSegm (S,a)) = ( InitSegm (T,a))

    proof

      assume that

       A1: a in S and

       A2: S is Initial_Segm of T;

      

       A3: S c= T by A2, Th29;

      thus ( InitSegm (S,a)) c= ( InitSegm (T,a))

      proof

        let x be object;

        assume x in ( InitSegm (S,a));

        then x in ( LowerCone {a}) & x in S by XBOOLE_0:def 4;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in ( InitSegm (T,a));

      then

       A5: x in ( LowerCone {a}) by XBOOLE_0:def 4;

      then

      consider a1 such that

       A6: x = a1 and

       A7: for a2 st a2 in {a} holds a1 < a2;

      

       A8: a1 in T by A4, A6, XBOOLE_0:def 4;

      a in {a} by TARSKI:def 1;

      then a1 < a by A7;

      then x in S by A1, A2, A6, A8, Th32;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    theorem :: ORDERS_2:34

    S c= T & the InternalRel of A well_orders T & (for a1, a2 st a2 in S & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T

    proof

      assume that

       A1: S c= T and

       A2: the InternalRel of A well_orders T and

       A3: for a1, a2 st a2 in S & a1 < a2 holds a1 in S and

       A4: S <> T;

      per cases ;

        case T <> {} ;

        set Y = (T \ S);

         not T c= S by A1, A4;

        then Y <> {} by XBOOLE_1: 37;

        then

        consider x be object such that

         A5: x in Y and

         A6: for y be object st y in Y holds [x, y] in the InternalRel of A by A2, WELLORD1: 5, XBOOLE_1: 36;

        reconsider x as Element of A by A5;

        take x;

        thus

         A7: x in T by A5, XBOOLE_0:def 5;

        S = (( LowerCone {x}) /\ T)

        proof

          thus S c= (( LowerCone {x}) /\ T)

          proof

            let y be object;

            assume

             A8: y in S;

            then

            reconsider a = y as Element of A;

            now

              let a1;

              assume that

               A9: a1 in {x} and

               A10: not a < a1;

              

               A11: a1 = x by A9, TARSKI:def 1;

              then

               A12: a1 <> a by A5, A8, XBOOLE_0:def 5;

              T is Chain of A by A2, Th13;

              then a1 <= a by A1, A7, A8, A10, A11, Th12;

              then a1 < a by A12;

              then a1 in S by A3, A8;

              hence contradiction by A5, A11, XBOOLE_0:def 5;

            end;

            then y in { a1 : for a2 st a2 in {x} holds a1 < a2 };

            hence thesis by A1, A8, XBOOLE_0:def 4;

          end;

          let y be object;

          assume

           A13: y in (( LowerCone {x}) /\ T);

          then y in ( LowerCone {x}) by XBOOLE_0:def 4;

          then

          consider a such that

           A14: a = y and

           A15: for a2 st a2 in {x} holds a < a2;

           A16:

          now

            assume y in Y;

            then [x, y] in the InternalRel of A by A6;

            then

             A17: x <= a by A14;

            x in {x} by TARSKI:def 1;

            hence contradiction by A15, A17, Th6;

          end;

          y in T by A13, XBOOLE_0:def 4;

          hence thesis by A16, XBOOLE_0:def 5;

        end;

        hence thesis;

      end;

        case T = {} ;

        hence thesis by A1;

      end;

    end;

    theorem :: ORDERS_2:35

    

     Th35: S c= T & the InternalRel of A well_orders T & (for a1, a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T

    proof

      assume that

       A1: S c= T and

       A2: the InternalRel of A well_orders T and

       A3: for a1, a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S and

       A4: S <> T;

      per cases ;

        case T <> {} ;

        set Y = (T \ S);

         not T c= S by A1, A4;

        then Y <> {} by XBOOLE_1: 37;

        then

        consider x be object such that

         A5: x in Y and

         A6: for y be object st y in Y holds [x, y] in the InternalRel of A by A2, WELLORD1: 5, XBOOLE_1: 36;

        reconsider x as Element of A by A5;

        take x;

        thus

         A7: x in T by A5, XBOOLE_0:def 5;

        S = (( LowerCone {x}) /\ T)

        proof

          thus S c= (( LowerCone {x}) /\ T)

          proof

            let y be object;

            assume

             A8: y in S;

            then

            reconsider a = y as Element of A;

            now

              let a1;

              assume that

               A9: a1 in {x} and

               A10: not a < a1;

              

               A11: a1 = x by A9, TARSKI:def 1;

              then

               A12: a1 <> a by A5, A8, XBOOLE_0:def 5;

              T is Chain of A by A2, Th13;

              then a1 <= a by A1, A7, A8, A10, A11, Th12;

              then a1 < a by A12;

              then a1 in S by A3, A7, A8, A11;

              hence contradiction by A5, A11, XBOOLE_0:def 5;

            end;

            then y in { a1 : for a2 st a2 in {x} holds a1 < a2 };

            hence thesis by A1, A8, XBOOLE_0:def 4;

          end;

          let y be object;

          assume

           A13: y in (( LowerCone {x}) /\ T);

          then y in ( LowerCone {x}) by XBOOLE_0:def 4;

          then

          consider a such that

           A14: a = y and

           A15: for a2 st a2 in {x} holds a < a2;

           A16:

          now

            assume y in Y;

            then [x, y] in the InternalRel of A by A6;

            then

             A17: x <= a by A14;

            x in {x} by TARSKI:def 1;

            hence contradiction by A15, A17, Th6;

          end;

          y in T by A13, XBOOLE_0:def 4;

          hence thesis by A16, XBOOLE_0:def 5;

        end;

        hence thesis;

      end;

        case T = {} ;

        hence thesis by A1;

      end;

    end;

    reserve f for Choice_Function of ( BOOL the carrier of A);

    definition

      let A;

      let f;

      :: ORDERS_2:def12

      mode Chain of f -> Chain of A means

      : Def12: it <> {} & the InternalRel of A well_orders it & for a st a in it holds (f . ( UpperCone ( InitSegm (it ,a)))) = a;

      existence

      proof

        set AC = the carrier of A;

        AC in ( BOOL AC) & not {} in ( BOOL AC) by ORDERS_1: 1, ORDERS_1: 2;

        then

        reconsider aa = (f . AC) as Element of A by ORDERS_1: 89;

        reconsider X = {aa} as Chain of A by Th8;

        take X;

        thus X <> {} ;

        

         A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;

        the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A by Def2, Def3;

        hence the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X by A1;

        the InternalRel of A is_strongly_connected_in X by Def7;

        hence the InternalRel of A is_connected_in X;

        thus the InternalRel of A is_well_founded_in X

        proof

          reconsider x = aa as set;

          let Y;

          assume that

           A2: Y c= X and

           A3: Y <> {} ;

          take x;

          Y = X by A2, A3, ZFMISC_1: 33;

          hence x in Y by TARSKI:def 1;

          thus ((the InternalRel of A -Seg x) /\ Y) c= {}

          proof

            let y be object;

            assume

             A4: y in ((the InternalRel of A -Seg x) /\ Y);

            then y in Y by XBOOLE_0:def 4;

            then

             A5: y = aa by A2, TARSKI:def 1;

            y in (the InternalRel of A -Seg x) by A4, XBOOLE_0:def 4;

            hence thesis by A5, WELLORD1: 1;

          end;

          thus thesis;

        end;

        let a;

        assume a in X;

        then

         A6: a = aa by TARSKI:def 1;

        (( LowerCone {a}) /\ X) c= ( {} A)

        proof

          let x be object;

          assume

           A7: x in (( LowerCone {a}) /\ X);

          then x in ( LowerCone {a}) by XBOOLE_0:def 4;

          then

           A8: ex a1 st x = a1 & for a2 st a2 in {a} holds a1 < a2;

          x in X by A7, XBOOLE_0:def 4;

          hence thesis by A6, A8;

        end;

        then (( LowerCone {a}) /\ X) = ( {} A);

        hence thesis by A6, Th14;

      end;

    end

    reserve fC,fC1,fC2 for Chain of f;

    theorem :: ORDERS_2:36

    

     Th36: {(f . the carrier of A)} is Chain of f

    proof

      set AC = the carrier of A;

      AC in ( BOOL AC) & not {} in ( BOOL AC) by ORDERS_1: 1, ORDERS_1: 2;

      then

      reconsider aa = (f . AC) as Element of A by ORDERS_1: 89;

      reconsider X = {aa} as Chain of A by Th8;

      

       A1: the InternalRel of A is_well_founded_in X

      proof

        reconsider x = aa as set;

        let Y;

        assume that

         A2: Y c= X and

         A3: Y <> {} ;

        take x;

        Y = X by A2, A3, ZFMISC_1: 33;

        hence x in Y by TARSKI:def 1;

        thus ((the InternalRel of A -Seg x) /\ Y) c= {}

        proof

          let y be object;

          assume

           A4: y in ((the InternalRel of A -Seg x) /\ Y);

          then y in Y by XBOOLE_0:def 4;

          then

           A5: y = aa by A2, TARSKI:def 1;

          y in (the InternalRel of A -Seg x) by A4, XBOOLE_0:def 4;

          hence thesis by A5, WELLORD1: 1;

        end;

        thus thesis;

      end;

      

       A6: for a st a in X holds (f . ( UpperCone ( InitSegm (X,a)))) = a

      proof

        let a;

        assume a in X;

        then

         A7: a = aa by TARSKI:def 1;

        (( LowerCone {a}) /\ X) c= ( {} A)

        proof

          let x be object;

          assume

           A8: x in (( LowerCone {a}) /\ X);

          then x in ( LowerCone {a}) by XBOOLE_0:def 4;

          then

           A9: ex a1 st x = a1 & for a2 st a2 in {a} holds a1 < a2;

          x in X by A8, XBOOLE_0:def 4;

          hence thesis by A7, A9;

        end;

        then (( LowerCone {a}) /\ X) = ( {} A);

        hence thesis by A7, Th14;

      end;

      the InternalRel of A is_strongly_connected_in X by Def7;

      then

       A10: the InternalRel of A is_connected_in X;

      the InternalRel of A is_antisymmetric_in the carrier of A by Def4;

      then

       A11: the InternalRel of A is_antisymmetric_in X;

      the InternalRel of A is_transitive_in the carrier of A by Def3;

      then

       A12: the InternalRel of A is_transitive_in X;

      the InternalRel of A is_reflexive_in the carrier of A by Def2;

      then the InternalRel of A is_reflexive_in X;

      then the InternalRel of A well_orders X by A12, A11, A10, A1;

      hence thesis by A6, Def12;

    end;

    theorem :: ORDERS_2:37

    

     Th37: (f . the carrier of A) in fC

    proof

      the InternalRel of A well_orders fC & fC <> {} by Def12;

      then

      consider x be object such that

       A1: x in fC and

       A2: for y be object st y in fC holds [x, y] in the InternalRel of A by WELLORD1: 5;

      reconsider x as Element of A by A1;

       A3:

      now

        set y = the Element of (( LowerCone {x}) /\ fC);

        assume

         A4: (( LowerCone {x}) /\ fC) <> ( {} A);

        then

        reconsider a = y as Element of A by Lm1;

        a in ( LowerCone {x}) by A4, XBOOLE_0:def 4;

        then

         A5: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2;

        y in fC by A4, XBOOLE_0:def 4;

        then [x, y] in the InternalRel of A by A2;

        then

         A6: x <= a;

        x in {x} by TARSKI:def 1;

        hence contradiction by A6, A5, Th6;

      end;

      (( LowerCone {x}) /\ fC) = ( InitSegm (fC,x));

      then (f . ( UpperCone (( LowerCone {x}) /\ fC))) = x by A1, Def12;

      hence thesis by A1, A3, Th14;

    end;

    theorem :: ORDERS_2:38

    

     Th38: a in fC & b = (f . the carrier of A) implies b <= a

    proof

      assume that

       A1: a in fC and

       A2: b = (f . the carrier of A);

      the InternalRel of A well_orders fC & fC <> {} by Def12;

      then

      consider x be object such that

       A3: x in fC and

       A4: for y be object st y in fC holds [x, y] in the InternalRel of A by WELLORD1: 5;

      reconsider x as Element of A by A3;

       A5:

      now

        set y = the Element of (( LowerCone {x}) /\ fC);

        assume

         A6: (( LowerCone {x}) /\ fC) <> ( {} A);

        then

        reconsider a = y as Element of A by Lm1;

        a in ( LowerCone {x}) by A6, XBOOLE_0:def 4;

        then

         A7: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2;

        y in fC by A6, XBOOLE_0:def 4;

        then [x, y] in the InternalRel of A by A4;

        then

         A8: x <= a;

        x in {x} by TARSKI:def 1;

        hence contradiction by A8, A7, Th6;

      end;

      (( LowerCone {x}) /\ fC) = ( InitSegm (fC,x));

      then (f . ( UpperCone (( LowerCone {x}) /\ fC))) = x by A3, Def12;

      then

       A9: (f . the carrier of A) = x by A5, Th14;

       [x, a] in the InternalRel of A by A1, A4;

      hence thesis by A2, A9;

    end;

    theorem :: ORDERS_2:39

    a = (f . the carrier of A) implies ( InitSegm (fC,a)) = {}

    proof

      set x = the Element of (( LowerCone {a}) /\ fC);

      assume

       A1: a = (f . the carrier of A);

      then

       A2: a in fC by Th37;

      assume

       A3: ( InitSegm (fC,a)) <> {} ;

      then

      reconsider b = x as Element of A by Lm1;

      x in ( LowerCone {a}) by A3, XBOOLE_0:def 4;

      then

       A4: ex a1 st a1 = b & for a2 st a2 in {a} holds a1 < a2;

      a in {a} by TARSKI:def 1;

      then

       A5: b < a by A4;

      

       A6: x in fC by A3, XBOOLE_0:def 4;

      then a <= b by A1, Th38;

      hence contradiction by A2, A6, A5, Th12;

    end;

    theorem :: ORDERS_2:40

    fC1 meets fC2

    proof

      (f . the carrier of A) in fC1 & (f . the carrier of A) in fC2 by Th37;

      hence thesis by XBOOLE_0: 3;

    end;

    theorem :: ORDERS_2:41

    

     Th41: fC1 <> fC2 implies (fC1 is Initial_Segm of fC2 iff not fC2 is Initial_Segm of fC1)

    proof

      assume

       A1: fC1 <> fC2;

      set N = { a : a in (fC1 /\ fC2) & ( InitSegm (fC1,a)) = ( InitSegm (fC2,a)) };

      

       A2: N c= fC1

      proof

        let x be object;

        assume x in N;

        then ex a st a = x & a in (fC1 /\ fC2) & ( InitSegm (fC1,a)) = ( InitSegm (fC2,a));

        hence thesis by XBOOLE_0:def 4;

      end;

      then

      reconsider N as Subset of A by XBOOLE_1: 1;

      

       A3: N c= fC2

      proof

        let x be object;

        assume x in N;

        then ex a st a = x & a in (fC1 /\ fC2) & ( InitSegm (fC1,a)) = ( InitSegm (fC2,a));

        hence thesis by XBOOLE_0:def 4;

      end;

       A4:

      now

        let a1, a2;

        assume that

         A5: a2 in N and

         A6: a1 in fC1 and

         A7: a1 < a2;

        

         A8: ex a st a = a2 & a in (fC1 /\ fC2) & ( InitSegm (fC1,a)) = ( InitSegm (fC2,a)) by A5;

        

         A9: ( InitSegm (fC1,a1)) = ( InitSegm (fC2,a1))

        proof

          thus ( InitSegm (fC1,a1)) c= ( InitSegm (fC2,a1))

          proof

            let x be object;

            assume

             A10: x in ( InitSegm (fC1,a1));

            then

            reconsider b = x as Element of A;

            

             A11: b in fC1 by A10, Th24;

            

             A12: b < a1 by A10, Th24;

            then b < a2 by A7, Th5;

            then b in ( InitSegm (fC1,a2)) by A11, Th24;

            then b in fC2 by A8, Th24;

            hence thesis by A12, Th24;

          end;

          let x be object;

          assume

           A13: x in ( InitSegm (fC2,a1));

          then

          reconsider b = x as Element of A;

          

           A14: b in fC2 by A13, Th24;

          

           A15: b < a1 by A13, Th24;

          then b < a2 by A7, Th5;

          then b in ( InitSegm (fC2,a2)) by A14, Th24;

          then b in fC1 by A8, Th24;

          hence thesis by A15, Th24;

        end;

        a1 in ( InitSegm (fC2,a2)) by A6, A7, A8, Th24;

        then a1 in fC2 by XBOOLE_0:def 4;

        then a1 in (fC1 /\ fC2) by A6, XBOOLE_0:def 4;

        hence a1 in N by A9;

      end;

       A16:

      now

        let a1, a2;

        assume that

         A17: a2 in N and

         A18: a1 in fC2 and

         A19: a1 < a2;

        

         A20: ex a st a = a2 & a in (fC1 /\ fC2) & ( InitSegm (fC1,a)) = ( InitSegm (fC2,a)) by A17;

        

         A21: ( InitSegm (fC1,a1)) = ( InitSegm (fC2,a1))

        proof

          thus ( InitSegm (fC1,a1)) c= ( InitSegm (fC2,a1))

          proof

            let x be object;

            assume

             A22: x in ( InitSegm (fC1,a1));

            then

            reconsider b = x as Element of A;

            

             A23: b in fC1 by A22, Th24;

            

             A24: b < a1 by A22, Th24;

            then b < a2 by A19, Th5;

            then b in ( InitSegm (fC1,a2)) by A23, Th24;

            then b in fC2 by A20, Th24;

            hence thesis by A24, Th24;

          end;

          let x be object;

          assume

           A25: x in ( InitSegm (fC2,a1));

          then

          reconsider b = x as Element of A;

          

           A26: b in fC2 by A25, Th24;

          

           A27: b < a1 by A25, Th24;

          then b < a2 by A19, Th5;

          then b in ( InitSegm (fC2,a2)) by A26, Th24;

          then b in fC1 by A20, Th24;

          hence thesis by A27, Th24;

        end;

        a1 in ( InitSegm (fC1,a2)) by A18, A19, A20, Th24;

        then a1 in fC1 by XBOOLE_0:def 4;

        then a1 in (fC1 /\ fC2) by A18, XBOOLE_0:def 4;

        hence a1 in N by A21;

      end;

      

       A28: the InternalRel of A well_orders fC1 & the InternalRel of A well_orders fC2 by Def12;

      now

        per cases by A2, A4, A28, A3, A16, Th35;

          suppose

           A29: N is Initial_Segm of fC1 & N = fC2;

          fC1 <> {} by Def12;

          hence thesis by A29, Th31;

        end;

          suppose

           A30: N is Initial_Segm of fC2 & N = fC1;

          fC2 <> {} by Def12;

          hence thesis by A30, Th31;

        end;

          suppose N = fC1 & N = fC2;

          hence thesis by A1;

        end;

          suppose

           A31: N is Initial_Segm of fC1 & N is Initial_Segm of fC2;

          fC2 <> {} by Def12;

          then

          consider b such that

           A32: b in fC2 and

           A33: N = ( InitSegm (fC2,b)) by A31, Def11;

          fC1 <> {} by Def12;

          then

          consider a such that

           A34: a in fC1 and

           A35: N = ( InitSegm (fC1,a)) by A31, Def11;

          

           A36: a = (f . ( UpperCone ( InitSegm (fC2,b)))) by A34, A35, A33, Def12

          .= b by A32, Def12;

          then a in (fC1 /\ fC2) by A34, A32, XBOOLE_0:def 4;

          then a in N by A35, A33, A36;

          hence thesis by A35, Th26;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDERS_2:42

    

     Th42: fC1 c< fC2 iff fC1 is Initial_Segm of fC2

    proof

      thus fC1 c< fC2 implies fC1 is Initial_Segm of fC2

      proof

        assume

         A1: fC1 c< fC2;

        now

          assume

           A2: fC2 is Initial_Segm of fC1;

          fC1 <> {} by Def12;

          then ex a st a in fC1 & fC2 = ( InitSegm (fC1,a)) by A2, Def11;

          then fC2 c= fC1 by XBOOLE_1: 17;

          hence contradiction by A1, XBOOLE_0:def 8;

        end;

        hence thesis by A1, Th41;

      end;

      assume

       A3: fC1 is Initial_Segm of fC2;

      

       A4: fC2 <> {} by Def12;

      then ex a st a in fC2 & fC1 = ( InitSegm (fC2,a)) by A3, Def11;

      then

       A5: fC1 c= fC2 by XBOOLE_1: 17;

      fC1 <> fC2 by A3, A4, Th30;

      hence thesis by A5;

    end;

    definition

      let A;

      let f;

      :: ORDERS_2:def13

      func Chains f -> set means

      : Def13: x in it iff x is Chain of f;

      existence

      proof

        defpred P[ set] means $1 is Chain of f;

        consider X such that

         A1: for x holds x in X iff x in ( bool the carrier of A) & P[x] from XFAMILY:sch 1;

        take X;

        let x;

        thus x in X implies x is Chain of f by A1;

        assume x is Chain of f;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let D1,D2 be set;

        assume

         A2: for x holds x in D1 iff x is Chain of f;

        assume

         A3: for x holds x in D2 iff x is Chain of f;

        thus D1 c= D2

        proof

          let x be object;

          assume x in D1;

          then x is Chain of f by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in D2;

        then x is Chain of f by A3;

        hence thesis by A2;

      end;

    end

    registration

      let A;

      let f;

      cluster ( Chains f) -> non empty;

      coherence

      proof

        set x = the Chain of f;

        x in ( Chains f) by Def13;

        hence thesis;

      end;

    end

    

     Lm2: ( union ( Chains f)) is Subset of A

    proof

      now

        let X;

        assume X in ( Chains f);

        then X is Chain of f by Def13;

        hence X c= the carrier of A;

      end;

      hence thesis by ZFMISC_1: 76;

    end;

    

     Lm3: ( union ( Chains f)) is Chain of A

    proof

      reconsider C = ( union ( Chains f)) as Subset of A by Lm2;

      the InternalRel of A is_strongly_connected_in C

      proof

        let x,y be object;

        assume that

         A1: x in C and

         A2: y in C;

        consider X such that

         A3: x in X and

         A4: X in ( Chains f) by A1, TARSKI:def 4;

        consider Y such that

         A5: y in Y and

         A6: Y in ( Chains f) by A2, TARSKI:def 4;

        reconsider X, Y as Chain of f by A4, A6, Def13;

        

         A7: the InternalRel of A is_strongly_connected_in X by Def7;

        

         A8: the InternalRel of A is_strongly_connected_in Y by Def7;

        now

          per cases ;

            suppose X = Y;

            hence thesis by A3, A5, A7;

          end;

            suppose

             A9: X <> Y;

            now

              per cases by A9, Th41;

                suppose X is Initial_Segm of Y;

                then X c< Y by Th42;

                then X c= Y;

                hence thesis by A3, A5, A8;

              end;

                suppose Y is Initial_Segm of X;

                then Y c< X by Th42;

                then Y c= X;

                hence thesis by A3, A5, A7;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by Def7;

    end;

    theorem :: ORDERS_2:43

    

     Th43: ( union ( Chains f)) <> {}

    proof

       {(f . the carrier of A)} is Chain of f by Th36;

      then {(f . the carrier of A)} in ( Chains f) by Def13;

      hence thesis by ORDERS_1: 6;

    end;

    theorem :: ORDERS_2:44

    

     Th44: fC <> ( union ( Chains f)) & S = ( union ( Chains f)) implies fC is Initial_Segm of S

    proof

      assume that

       A1: fC <> ( union ( Chains f)) and

       A2: S = ( union ( Chains f));

      set x = the Element of (S \ fC);

      fC in ( Chains f) by Def13;

      then fC c= ( union ( Chains f)) by ZFMISC_1: 74;

      then not ( union ( Chains f)) c= fC by A1;

      then

       A3: (S \ fC) <> {} by A2, XBOOLE_1: 37;

      then

       A4: not x in fC by XBOOLE_0:def 5;

      x in S by A3, XBOOLE_0:def 5;

      then

      consider X such that

       A5: x in X and

       A6: X in ( Chains f) by A2, TARSKI:def 4;

      reconsider X as Chain of f by A6, Def13;

       not X c= fC by A3, A5, XBOOLE_0:def 5;

      then not X c< fC;

      then not X is Initial_Segm of fC by Th42;

      then fC is Initial_Segm of X by A5, A4, Th41;

      then

      consider a such that

       A7: a in X and

       A8: fC = ( InitSegm (X,a)) by A5, Def11;

      

       A9: X c= S by A2, A6, ZFMISC_1: 74;

      ( InitSegm (S,a)) = ( InitSegm (X,a))

      proof

        thus ( InitSegm (S,a)) c= ( InitSegm (X,a))

        proof

          let x be object;

          assume

           A10: x in ( InitSegm (S,a));

          then

           A11: x in ( LowerCone {a}) by XBOOLE_0:def 4;

          then

          consider b such that

           A12: b = x and

           A13: for a2 st a2 in {a} holds b < a2;

          b in S by A10, A12, XBOOLE_0:def 4;

          then

          consider Y such that

           A14: b in Y and

           A15: Y in ( Chains f) by A2, TARSKI:def 4;

          reconsider Y as Chain of f by A15, Def13;

          a in {a} by TARSKI:def 1;

          then

           A16: b < a by A13;

          now

            per cases ;

              suppose X = Y;

              hence thesis by A11, A12, A14, XBOOLE_0:def 4;

            end;

              suppose

               A17: X <> Y;

              now

                per cases by A17, Th41;

                  suppose X is Initial_Segm of Y;

                  then x in X by A7, A12, A16, A14, Th32;

                  hence thesis by A11, XBOOLE_0:def 4;

                end;

                  suppose Y is Initial_Segm of X;

                  then Y c< X by Th42;

                  then Y c= X;

                  hence thesis by A11, A12, A14, XBOOLE_0:def 4;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        let x be object;

        assume x in ( InitSegm (X,a));

        then x in ( LowerCone {a}) & x in X by XBOOLE_0:def 4;

        hence thesis by A9, XBOOLE_0:def 4;

      end;

      hence thesis by A7, A8, A9, Def11;

    end;

    theorem :: ORDERS_2:45

    

     Th45: ( union ( Chains f)) is Chain of f

    proof

      reconsider C = ( union ( Chains f)) as Chain of A by Lm3;

       A1:

      now

        let a;

        assume a in C;

        then

        consider X such that

         A2: a in X and

         A3: X in ( Chains f) by TARSKI:def 4;

        reconsider X as Chain of f by A3, Def13;

        now

          ( InitSegm (C,a)) = ( InitSegm (X,a)) by A2, Th33, Th44;

          hence (f . ( UpperCone ( InitSegm (C,a)))) = a by A2, Def12;

        end;

        hence (f . ( UpperCone ( InitSegm (C,a)))) = a;

      end;

      

       A4: the InternalRel of A well_orders C

      proof

        

         A5: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;

        the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A by Def2, Def3;

        hence the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C by A5;

        the InternalRel of A is_strongly_connected_in C by Def7;

        hence the InternalRel of A is_connected_in C;

        let Y;

        set x = the Element of Y;

        assume that

         A6: Y c= C and

         A7: Y <> {} ;

        x in C by A6, A7;

        then

        consider X such that

         A8: x in X and

         A9: X in ( Chains f) by TARSKI:def 4;

        reconsider X as Chain of f by A9, Def13;

        

         A10: the InternalRel of A well_orders X by Def12;

        (X /\ Y) <> {} by A7, A8, XBOOLE_0:def 4;

        then

        consider a be object such that

         A11: a in (X /\ Y) and

         A12: for x be object st x in (X /\ Y) holds [a, x] in the InternalRel of A by A10, WELLORD1: 5, XBOOLE_1: 17;

        take a;

        thus a in Y by A11, XBOOLE_0:def 4;

        reconsider aa = a as Element of A by A11;

        thus ((the InternalRel of A -Seg a) /\ Y) c= {}

        proof

          let y be object;

          assume

           A13: y in ((the InternalRel of A -Seg a) /\ Y);

          then

           A14: y in Y by XBOOLE_0:def 4;

          then y in C by A6;

          then

          reconsider b = y as Element of A;

          

           A15: y in (the InternalRel of A -Seg a) by A13, XBOOLE_0:def 4;

          then

           A16: y <> a by WELLORD1: 1;

           [y, a] in the InternalRel of A by A15, WELLORD1: 1;

          then

           A17: b <= aa;

          now

            per cases ;

              suppose

               A18: X <> C;

              a in X & b < aa by A11, A16, A17, XBOOLE_0:def 4;

              hence y in X by A6, A14, A18, Th32, Th44;

            end;

              suppose X = C;

              hence y in X by A6, A14;

            end;

          end;

          then y in (X /\ Y) by A14, XBOOLE_0:def 4;

          then [a, y] in the InternalRel of A by A12;

          then aa <= b;

          hence thesis by A16, A17, Th2;

        end;

        thus thesis;

      end;

      C <> {} by Th43;

      hence thesis by A4, A1, Def12;

    end;

    begin

    reserve R for Relation,

A for non empty Poset,

C for Chain of A,

S for Subset of A,

a,a1,a2,b,c1,c2 for Element of A;

    theorem :: ORDERS_2:46

    

     Th46: ( field (the InternalRel of A |_2 S)) = S

    proof

      set P = (the InternalRel of A |_2 S);

      thus ( field P) c= S by WELLORD1: 13;

      thus S c= ( field P)

      proof

        let x be object;

        assume

         A1: x in S;

        then

         A2: [x, x] in [:S, S:] by ZFMISC_1: 87;

        the InternalRel of A is_reflexive_in the carrier of A by Def2;

        then [x, x] in the InternalRel of A by A1;

        then [x, x] in P by A2, XBOOLE_0:def 4;

        then x in ( dom P) by XTUPLE_0:def 12;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: ORDERS_2:47

    (the InternalRel of A |_2 S) is being_linear-order implies S is Chain of A

    proof

      assume (the InternalRel of A |_2 S) is being_linear-order;

      then

       A1: (the InternalRel of A |_2 S) is connected;

      ( field (the InternalRel of A |_2 S)) = S by Th46;

      then

       A2: (the InternalRel of A |_2 S) is_connected_in S by A1;

      S is strongly_connected

      proof

        let x,y be object;

        assume

         A3: x in S & y in S;

        then

        reconsider a = x, b = y as Element of A;

        now

          per cases ;

            suppose x = y;

            then a <= b;

            hence thesis;

          end;

            suppose x <> y;

            then [x, y] in (the InternalRel of A |_2 S) or [y, x] in (the InternalRel of A |_2 S) by A2, A3;

            hence thesis by XBOOLE_0:def 4;

          end;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: ORDERS_2:48

    (the InternalRel of A |_2 C) is being_linear-order

    proof

      set P = (the InternalRel of A |_2 C);

      

       A1: P is_connected_in C

      proof

        let x,y be object;

        assume

         A2: x in C & y in C;

        then

         A3: [x, y] in [:C, C:] & [y, x] in [:C, C:] by ZFMISC_1: 87;

        the InternalRel of A is_strongly_connected_in C by Def7;

        then [x, y] in the InternalRel of A or [y, x] in the InternalRel of A by A2;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      the InternalRel of A is being_partial-order;

      then P is being_partial-order by ORDERS_1: 26;

      hence P is reflexive & P is transitive & P is antisymmetric;

      C = ( field P) by Th46;

      hence thesis by A1;

    end;

    theorem :: ORDERS_2:49

    the InternalRel of A linearly_orders S implies S is Chain of A by ORDERS_1: 7, Def7;

    theorem :: ORDERS_2:50

    the InternalRel of A linearly_orders C

    proof

      

       A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;

      the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A by Def2, Def3;

      hence the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C by A1;

      the InternalRel of A is_strongly_connected_in C by Def7;

      hence thesis;

    end;

    theorem :: ORDERS_2:51

    a is_minimal_in the InternalRel of A iff for b holds not b < a

    proof

      

       A1: the carrier of A = ( field the InternalRel of A) by ORDERS_1: 15;

      thus a is_minimal_in the InternalRel of A implies for b holds not b < a

      proof

        assume

         A2: a is_minimal_in the InternalRel of A;

        let b;

        a = b or not [b, a] in the InternalRel of A by A1, A2;

        then a = b or not b <= a;

        hence thesis;

      end;

      assume

       A3: for b holds not b < a;

      thus a in ( field the InternalRel of A) by A1;

      let y;

      assume that

       A4: y in ( field the InternalRel of A) and

       A5: y <> a and

       A6: [y, a] in the InternalRel of A;

      reconsider b = y as Element of A by A4, ORDERS_1: 15;

      b <= a by A6;

      then b < a by A5;

      hence thesis by A3;

    end;

    theorem :: ORDERS_2:52

    a is_maximal_in the InternalRel of A iff for b holds not a < b

    proof

      

       A1: the carrier of A = ( field the InternalRel of A) by ORDERS_1: 15;

      thus a is_maximal_in the InternalRel of A implies for b holds not a < b

      proof

        assume

         A2: a is_maximal_in the InternalRel of A;

        let b;

        a = b or not [a, b] in the InternalRel of A by A1, A2;

        then a = b or not a <= b;

        hence thesis;

      end;

      assume

       A3: for b holds not a < b;

      thus a in ( field the InternalRel of A) by A1;

      let y;

      assume that

       A4: y in ( field the InternalRel of A) and

       A5: y <> a and

       A6: [a, y] in the InternalRel of A;

      reconsider b = y as Element of A by A4, ORDERS_1: 15;

      a <= b by A6;

      then a < b by A5;

      hence thesis by A3;

    end;

    theorem :: ORDERS_2:53

    a is_superior_of the InternalRel of A iff for b st a <> b holds b < a

    proof

      

       A1: the carrier of A = ( field the InternalRel of A) by ORDERS_1: 15;

      thus a is_superior_of the InternalRel of A implies for b st a <> b holds b < a

      proof

        assume

         A2: a is_superior_of the InternalRel of A;

        let b;

        assume

         A3: a <> b;

        then [b, a] in the InternalRel of A by A1, A2;

        then b <= a;

        hence thesis by A3;

      end;

      assume

       A4: for b st a <> b holds b < a;

      thus a in ( field the InternalRel of A) by A1;

      let y;

      assume y in ( field the InternalRel of A);

      then

      reconsider b = y as Element of A by ORDERS_1: 15;

      assume y <> a;

      then b < a by A4;

      then b <= a;

      hence thesis;

    end;

    theorem :: ORDERS_2:54

    a is_inferior_of the InternalRel of A iff for b st a <> b holds a < b

    proof

      

       A1: the carrier of A = ( field the InternalRel of A) by ORDERS_1: 15;

      thus a is_inferior_of the InternalRel of A implies for b st a <> b holds a < b

      proof

        assume

         A2: a is_inferior_of the InternalRel of A;

        let b;

        assume

         A3: a <> b;

        then [a, b] in the InternalRel of A by A1, A2;

        then a <= b;

        hence thesis by A3;

      end;

      assume

       A4: for b st a <> b holds a < b;

      thus a in ( field the InternalRel of A) by A1;

      let y;

      assume y in ( field the InternalRel of A);

      then

      reconsider b = y as Element of A by ORDERS_1: 15;

      assume y <> a;

      then a < b by A4;

      then a <= b;

      hence thesis;

    end;

    

     Lm4: R well_orders X & Y c= X implies R well_orders Y

    proof

      assume that

       A1: R well_orders X and

       A2: Y c= X;

      

       A3: R is_antisymmetric_in X & R is_connected_in X by A1;

      

       A4: R is_well_founded_in X by A1;

      R is_reflexive_in X & R is_transitive_in X by A1;

      hence R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y & R is_connected_in Y by A2, A3;

      let Z be set;

      assume that

       A5: Z c= Y and

       A6: Z <> {} ;

      Z c= X by A2, A5;

      hence thesis by A6, A4;

    end;

    theorem :: ORDERS_2:55

    

     Th55: (for C holds ex a st for b st b in C holds b <= a) implies ex a st for b holds not a < b

    proof

      set f = the Choice_Function of ( BOOL the carrier of A);

      reconsider F = ( union ( Chains f)) as Chain of f by Th45;

      assume for C holds ex a st for b st b in C holds b <= a;

      then

      consider a such that

       A1: for b st b in F holds b <= a;

      take a;

      let b;

      assume

       A2: a < b;

      now

        let a1;

        assume a1 in F;

        then a1 <= a by A1;

        hence a1 < b by A2, Th7;

      end;

      then b in { a1 : for a2 st a2 in F holds a2 < a1 };

      then not ( UpperCone F) in { {} } by TARSKI:def 1;

      then

       A3: ( UpperCone F) in ( BOOL the carrier of A) by XBOOLE_0:def 5;

       not {} in ( BOOL the carrier of A) by ORDERS_1: 1;

      then

       A4: (f . ( UpperCone F)) in ( UpperCone F) by A3, ORDERS_1: 89;

      then

      reconsider c = (f . ( UpperCone F)) as Element of A;

      reconsider Z = (F \/ {c}) as Subset of A;

      

       A5: ex c11 be Element of A st c11 = c & for a2 st a2 in F holds a2 < c11 by A4;

      

       A6: the InternalRel of A is_connected_in Z

      proof

        let x,y be object;

        assume

         A7: x in Z & y in Z;

        then

        reconsider x1 = x, y1 = y as Element of A;

        now

          per cases by A7, XBOOLE_0:def 3;

            suppose x1 in F & y1 in F;

            then x1 <= y1 or y1 <= x1 by Th11;

            hence thesis;

          end;

            suppose

             A8: x1 in F & y1 in {c};

            then y1 = c by TARSKI:def 1;

            then x1 < y1 by A5, A8;

            then x1 <= y1;

            hence thesis;

          end;

            suppose

             A9: x1 in {c} & y1 in F;

            then x1 = c by TARSKI:def 1;

            then y1 < x1 by A5, A9;

            then y1 <= x1;

            hence thesis;

          end;

            suppose

             A10: x1 in {c} & y1 in {c};

            then x1 = c by TARSKI:def 1;

            hence thesis by A10, TARSKI:def 1;

          end;

        end;

        hence thesis;

      end;

       A11:

      now

        let a1;

        assume

         A12: a1 in Z;

        now

          per cases ;

            suppose

             A13: a1 = c;

            ( InitSegm (Z,c)) = F

            proof

              thus ( InitSegm (Z,c)) c= F

              proof

                let x be object;

                assume that

                 A14: x in ( InitSegm (Z,c)) and

                 A15: not x in F;

                x in Z by A14, XBOOLE_0:def 4;

                then x in {c} by A15, XBOOLE_0:def 3;

                then

                 A16: x = c by TARSKI:def 1;

                x in ( LowerCone {c}) by A14, XBOOLE_0:def 4;

                hence contradiction by A16, Th21;

              end;

              let x be object;

              assume

               A17: x in F;

              then

              reconsider y = x as Element of A;

              y < c by A5, A17;

              then

               A18: x in ( LowerCone {c}) by Th23;

              x in Z by A17, XBOOLE_0:def 3;

              hence thesis by A18, XBOOLE_0:def 4;

            end;

            hence (f . ( UpperCone ( InitSegm (Z,a1)))) = a1 by A13;

          end;

            suppose a1 <> c;

            then not a1 in {c} by TARSKI:def 1;

            then

             A19: a1 in F by A12, XBOOLE_0:def 3;

            

             A20: ( InitSegm (Z,a1)) c= ( InitSegm (F,a1))

            proof

              let x be object;

              assume

               A21: x in ( InitSegm (Z,a1));

              then

               A22: x in ( LowerCone {a1}) by XBOOLE_0:def 4;

              now

                assume

                 A23: not x in F;

                x in Z by A21, XBOOLE_0:def 4;

                then x in {c} by A23, XBOOLE_0:def 3;

                then x = c by TARSKI:def 1;

                then

                 A24: ex c1 st c1 = c & for c2 st c2 in {a1} holds c1 < c2 by A22;

                

                 A25: a1 < c by A5, A19;

                a1 in {a1} by TARSKI:def 1;

                then c < a1 by A24;

                hence contradiction by A25, Th4;

              end;

              hence thesis by A22, XBOOLE_0:def 4;

            end;

            ( InitSegm (F,a1)) c= ( InitSegm (Z,a1)) by Th28, XBOOLE_1: 7;

            then ( InitSegm (Z,a1)) = ( InitSegm (F,a1)) by A20;

            hence (f . ( UpperCone ( InitSegm (Z,a1)))) = a1 by A19, Def12;

          end;

        end;

        hence (f . ( UpperCone ( InitSegm (Z,a1)))) = a1;

      end;

      the InternalRel of A is_reflexive_in the carrier of A by Def2;

      then

       A26: the InternalRel of A is_reflexive_in Z;

      then the InternalRel of A is_strongly_connected_in Z by A6, ORDERS_1: 7;

      then

       A27: Z is Chain of A by Def7;

      

       A28: the InternalRel of A is_well_founded_in Z

      proof

        let Y;

        assume that

         A29: Y c= Z and

         A30: Y <> {} ;

        now

          per cases ;

            case

             A31: Y = {c};

            take x = c;

            thus x in Y by A31, TARSKI:def 1;

            assume (the InternalRel of A -Seg x) meets Y;

            then

            consider x9 be object such that

             A32: x9 in (the InternalRel of A -Seg x) and

             A33: x9 in Y by XBOOLE_0: 3;

            x9 = c by A31, A33, TARSKI:def 1;

            hence contradiction by A32, WELLORD1: 1;

          end;

            case

             A34: Y <> {c};

            set X = (Y \ {c});

             A35:

            now

              assume X = {} ;

              then Y c= {c} by XBOOLE_1: 37;

              hence contradiction by A30, A34, ZFMISC_1: 33;

            end;

            

             A36: X c= F

            proof

              let x be object;

              assume that

               A37: x in X and

               A38: not x in F;

              x in Y by A37;

              then x in {c} by A29, A38, XBOOLE_0:def 3;

              hence thesis by A37, XBOOLE_0:def 5;

            end;

            the InternalRel of A well_orders F by Def12;

            then the InternalRel of A well_orders X by A36, Lm4;

            then the InternalRel of A is_well_founded_in X;

            then

            consider x be object such that

             A39: x in X and

             A40: (the InternalRel of A -Seg x) misses X by A35;

            take x9 = x;

            thus x9 in Y by A39;

            

             A41: ((the InternalRel of A -Seg x) /\ X) = {} by A40;

            now

              per cases ;

                suppose

                 A42: c in Y;

                 A43:

                now

                  x9 in F by A36, A39;

                  then

                  reconsider x99 = x9 as Element of A;

                  assume

                   A44: c in (the InternalRel of A -Seg x9);

                  then [c, x9] in the InternalRel of A by WELLORD1: 1;

                  then

                   A45: c <= x99;

                  

                   A46: x99 < c by A5, A36, A39;

                  c <> x99 by A44, WELLORD1: 1;

                  then c < x99 by A45;

                  hence contradiction by A46, Th4;

                end;

                 A47:

                now

                  set x = the Element of ((the InternalRel of A -Seg x9) /\ {c});

                  assume

                   A48: ((the InternalRel of A -Seg x9) /\ {c}) <> {} ;

                  then x in {c} by XBOOLE_0:def 4;

                  then x = c by TARSKI:def 1;

                  hence contradiction by A43, A48, XBOOLE_0:def 4;

                end;

                 {c} c= Y by A42, ZFMISC_1: 31;

                then Y = (X \/ {c}) by XBOOLE_1: 45;

                

                then ((the InternalRel of A -Seg x9) /\ Y) = ( {} \/ {} ) by A41, A47, XBOOLE_1: 23

                .= {} ;

                hence (the InternalRel of A -Seg x9) misses Y;

              end;

                suppose not c in Y;

                then Y misses {c} by ZFMISC_1: 50;

                hence (the InternalRel of A -Seg x9) misses Y by A40, XBOOLE_1: 83;

              end;

            end;

            hence (the InternalRel of A -Seg x9) misses Y;

          end;

        end;

        hence thesis;

      end;

      the InternalRel of A is_transitive_in the carrier of A by Def3;

      then

       A49: the InternalRel of A is_transitive_in Z;

      the InternalRel of A is_antisymmetric_in the carrier of A by Def4;

      then the InternalRel of A is_antisymmetric_in Z;

      then the InternalRel of A well_orders Z by A26, A49, A6, A28;

      then

      reconsider Z as Chain of f by A27, A11, Def12;

      c in {c} by TARSKI:def 1;

      then

       A50: c in Z by XBOOLE_0:def 3;

      Z in ( Chains f) by Def13;

      then c in F by A50, TARSKI:def 4;

      hence thesis by A5;

    end;

    theorem :: ORDERS_2:56

    (for C holds ex a st for b st b in C holds a <= b) implies ex a st for b holds not b < a

    proof

      set X = the carrier of A;

      set R = (the InternalRel of A ~ );

      

       A1: ( dom R) = ( dom the InternalRel of A) by RELAT_2: 12

      .= X by PARTFUN1:def 2;

      

       A2: for a,b be Element of A holds [a, b] in R iff b <= a by RELAT_1:def 7;

      reconsider R as Order of the carrier of A by A1, PARTFUN1:def 2;

      set B = RelStr (# the carrier of A, R #);

      assume

       A3: for C holds ex a st for b st b in C holds a <= b;

      for E be Chain of B holds ex e be Element of B st for f be Element of B st f in E holds f <= e

      proof

        let E be Chain of B;

        reconsider C = E as Subset of A;

        the InternalRel of A is_strongly_connected_in C

        proof

          let x,y be object;

          assume

           A4: x in C & y in C;

          then

          reconsider e = x, f = y as Element of B;

          reconsider e1 = e, f1 = f as Element of A;

          

           A5: e <= f or f <= e by A4, Th11;

          now

            per cases by A5;

              suppose [e, f] in R;

              then f1 <= e1 by A2;

              hence thesis;

            end;

              suppose [f, e] in R;

              then e1 <= f1 by A2;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

        reconsider C as Chain of A by Def7;

        consider a such that

         A6: for b st b in C holds a <= b by A3;

        reconsider e = a as Element of B;

        take e;

        let f be Element of B;

        reconsider b = f as Element of A;

        assume f in E;

        then a <= b by A6;

        then [f, e] in R by A2;

        hence thesis;

      end;

      then

      consider e be Element of B such that

       A7: for f be Element of B holds not e < f by Th55;

      reconsider d = e as Element of A;

      take d;

      let b;

      reconsider f = b as Element of B;

      assume

       A8: b < d;

      then b <= d;

      then [e, f] in R by A2;

      then e <= f;

      then e < f by A8;

      hence thesis by A7;

    end;

    registration

      cluster strict empty for RelStr;

      existence

      proof

        take R = RelStr (# {} , the Relation of {} #);

        thus R is strict;

        thus the carrier of R is empty;

      end;

    end