orders_1.miz



    begin

    reserve X,Y for set,

x,x1,x2,y,y1,y2,z for set,

f,g,h for Function;

    

     Lm1: (ex X st X <> {} & X in Y) iff ( union Y) <> {}

    proof

      thus (ex X st X <> {} & X in Y) implies ( union Y) <> {}

      proof

        given X such that

         A1: X <> {} and

         A2: X in Y;

        set x = the Element of X;

        x in X by A1;

        hence thesis by A2, TARSKI:def 4;

      end;

      set x = the Element of ( union Y);

      assume ( union Y) <> {} ;

      then

      consider X such that

       A3: x in X and

       A4: X in Y by TARSKI:def 4;

      take X;

      thus thesis by A3, A4;

    end;

    definition

      let f be Function;

      :: ORDERS_1:def1

      mode Choice of f -> Function means

      : Def1: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = the Element of (f . x);

      existence

      proof

        deffunc F( object) = the Element of (f . $1);

        consider g be Function such that

         A1: ( dom g) = ( dom f) and

         A2: for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        take g;

        thus ( dom g) = ( dom f) by A1;

        let x be object such that

         A3: x in ( dom f);

        reconsider x as set by TARSKI: 1;

        (g . x) = F(x) by A3, A2;

        hence thesis;

      end;

    end

    definition

      let I be set;

      let M be ManySortedSet of I;

      :: original: Choice

      redefine

      :: ORDERS_1:def2

      mode Choice of M -> ManySortedSet of I means

      : Def2: for x be object st x in I holds (it . x) = the Element of (M . x);

      coherence

      proof

        let Ch be Choice of M;

        ( dom Ch) = ( dom M) by Def1

        .= I by PARTFUN1:def 2;

        then Ch is totalI -defined Function by RELAT_1:def 18, PARTFUN1:def 2;

        hence thesis;

      end;

      compatibility

      proof

        let Ch be ManySortedSet of I;

        ( dom M) = I by PARTFUN1:def 2;

        hence Ch is Choice of M implies for x be object st x in I holds (Ch . x) = the Element of (M . x) by Def1;

        assume

         A1: for x be object st x in I holds (Ch . x) = the Element of (M . x);

        

        thus ( dom Ch) = I by PARTFUN1:def 2

        .= ( dom M) by PARTFUN1:def 2;

        thus for x be object st x in ( dom M) holds (Ch . x) = the Element of (M . x) by A1;

      end;

    end

    definition

      let A be set;

      mode Choice_Function of A is Choice of ( id A);

    end

    reserve M for non empty set;

    

     Lm2: not {} in M implies for Ch be Choice_Function of M holds for X st X in M holds (Ch . X) in X

    proof

      assume

       A1: not {} in M;

      let Ch be Choice_Function of M;

      let X;

      assume

       A2: X in M;

      then

       A3: X <> {} by A1;

      

       A4: (( id M) . X) = X by A2, FUNCT_1: 18;

      X in ( dom Ch) by A2, PARTFUN1:def 2;

      

      then (Ch . X) = the Element of (( id M) . X) by Def2

      .= the Element of X by A4;

      hence (Ch . X) in X by A3;

    end;

    

     Lm3: not {} in M implies for Ch be Choice_Function of M holds Ch is Function of M, ( union M)

    proof

      assume

       A1: not {} in M;

      let Ch be Choice_Function of M;

      

       A2: ( dom Ch) = M by PARTFUN1:def 2;

      ( rng Ch) c= ( union M)

      proof

        let x be object;

        assume x in ( rng Ch);

        then

        consider y be object such that

         A3: y in ( dom Ch) and

         A4: x = (Ch . y) by FUNCT_1:def 3;

        reconsider y as set by TARSKI: 1;

        

         A5: x in y by A3, A1, A4, Lm2;

        y in M by A3;

        hence x in ( union M) by A5, TARSKI:def 4;

      end;

      hence Ch is Function of M, ( union M) by A2, FUNCT_2: 2;

    end;

    reserve D for non empty set;

    definition

      let D be set;

      :: ORDERS_1:def3

      func BOOL D -> set equals (( bool D) \ { {} });

      coherence ;

    end

    registration

      let D;

      cluster ( BOOL D) -> non empty;

      coherence

      proof

        

         A1: not D in { {} } by TARSKI:def 1;

        D in ( bool D) by ZFMISC_1:def 1;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

    end

    theorem :: ORDERS_1:1

     not {} in ( BOOL D)

    proof

      assume not thesis;

      then not {} in { {} } by XBOOLE_0:def 5;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: ORDERS_1:2

    D c= X iff D in ( BOOL X)

    proof

      thus D c= X implies D in ( BOOL X)

      proof

        

         A1: not D in { {} } by TARSKI:def 1;

        assume D c= X;

        hence thesis by A1, XBOOLE_0:def 5;

      end;

      assume D in ( BOOL X);

      hence thesis;

    end;

    reserve P for Relation;

    definition

      let X;

      mode Order of X is total reflexive antisymmetric transitive Relation of X;

    end

    reserve O for Order of X;

    

     Lm4: for R be total Relation of X holds ( field R) = X

    proof

      let R be total Relation of X;

      

      thus ( field R) = (X \/ ( rng R)) by PARTFUN1:def 2

      .= X by XBOOLE_1: 12;

    end;

    theorem :: ORDERS_1:3

    

     Th3: x in X implies [x, x] in O

    proof

      ( field O) = X by Lm4;

      then O is_reflexive_in X by RELAT_2:def 9;

      hence thesis;

    end;

    theorem :: ORDERS_1:4

    x in X & y in X & [x, y] in O & [y, x] in O implies x = y

    proof

      ( field O) = X by Lm4;

      then O is_antisymmetric_in X by RELAT_2:def 12;

      hence thesis;

    end;

    theorem :: ORDERS_1:5

    x in X & y in X & z in X & [x, y] in O & [y, z] in O implies [x, z] in O

    proof

      ( field O) = X by Lm4;

      then O is_transitive_in X by RELAT_2:def 16;

      hence thesis;

    end;

    theorem :: ORDERS_1:6

    (ex X st X <> {} & X in Y) iff ( union Y) <> {} by Lm1;

    theorem :: ORDERS_1:7

    P is_strongly_connected_in X iff P is_reflexive_in X & P is_connected_in X

    proof

      thus P is_strongly_connected_in X implies P is_reflexive_in X & P is_connected_in X;

      assume that

       A1: P is_reflexive_in X and

       A2: P is_connected_in X;

      let x,y be object;

      assume that

       A3: x in X and

       A4: y in X;

      x = y implies thesis by A1, A3;

      hence thesis by A2, A3, A4;

    end;

    theorem :: ORDERS_1:8

    P is_reflexive_in X & Y c= X implies P is_reflexive_in Y;

    theorem :: ORDERS_1:9

    P is_antisymmetric_in X & Y c= X implies P is_antisymmetric_in Y;

    theorem :: ORDERS_1:10

    P is_transitive_in X & Y c= X implies P is_transitive_in Y;

    theorem :: ORDERS_1:11

    P is_strongly_connected_in X & Y c= X implies P is_strongly_connected_in Y;

    theorem :: ORDERS_1:12

    for R be total Relation of X holds ( field R) = X by Lm4;

    theorem :: ORDERS_1:13

    

     Th13: for A be set, R be Relation of A st R is_reflexive_in A holds ( dom R) = A & ( field R) = A

    proof

      let A be set, R be Relation of A such that

       A1: R is_reflexive_in A;

      

       A2: A c= ( dom R)

      proof

        let x be object;

        assume x in A;

        then [x, x] in R by A1;

        hence thesis by XTUPLE_0:def 12;

      end;

      hence ( dom R) = A;

      

      thus ( field R) = (A \/ ( rng R)) by A2, XBOOLE_0:def 10

      .= A by XBOOLE_1: 12;

    end;

    begin

    reserve R,P for Relation,

X,X1,X2,Y,Z,x,y,z,u for set,

g,h for Function,

O for Order of X,

D for non empty set,

d,d1,d2 for Element of D,

A1,A2,B for Ordinal,

L,L1,L2 for Sequence;

    theorem :: ORDERS_1:14

    

     Th14: ( dom O) = X & ( rng O) = X

    proof

      thus ( dom O) = X

      proof

        thus ( dom O) c= X;

        let x be object;

        assume x in X;

        then [x, x] in O by Th3;

        hence thesis by XTUPLE_0:def 12;

      end;

      thus ( rng O) c= X;

      let x be object;

      assume x in X;

      then [x, x] in O by Th3;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: ORDERS_1:15

    ( field O) = X

    proof

      

      thus X = (X \/ X)

      .= (( dom O) \/ X) by Th14

      .= ( field O) by Th14;

    end;

    definition

      let R;

      :: ORDERS_1:def4

      attr R is being_quasi-order means R is reflexive transitive;

      :: ORDERS_1:def5

      attr R is being_partial-order means R is reflexive transitive antisymmetric;

      :: ORDERS_1:def6

      attr R is being_linear-order means R is reflexive transitive antisymmetric connected;

    end

    theorem :: ORDERS_1:16

    R is being_quasi-order implies (R ~ ) is being_quasi-order;

    theorem :: ORDERS_1:17

    R is being_partial-order implies (R ~ ) is being_partial-order;

    

     Lm5: R is connected implies (R ~ ) is connected

    proof

      assume

       A1: for x,y be object holds x in ( field R) & y in ( field R) & x <> y implies [x, y] in R or [y, x] in R;

      let x,y be object;

      assume that

       A2: x in ( field (R ~ )) and

       A3: y in ( field (R ~ )) and

       A4: x <> y;

      ( field R) = ( field (R ~ )) by RELAT_1: 21;

      then [x, y] in R or [y, x] in R by A1, A2, A3, A4;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: ORDERS_1:18

    

     Th18: R is being_linear-order implies (R ~ ) is being_linear-order by Lm5;

    theorem :: ORDERS_1:19

    R is well-ordering implies R is being_quasi-order & R is being_partial-order & R is being_linear-order;

    theorem :: ORDERS_1:20

    R is being_linear-order implies R is being_quasi-order & R is being_partial-order;

    theorem :: ORDERS_1:21

    R is being_partial-order implies R is being_quasi-order;

    theorem :: ORDERS_1:22

    O is being_partial-order;

    theorem :: ORDERS_1:23

    O is being_quasi-order;

    theorem :: ORDERS_1:24

    O is connected implies O is being_linear-order;

    

     Lm6: R c= [:( field R), ( field R):]

    proof

      let y,z be object;

      assume

       A1: [y, z] in R;

      then

       A2: z in ( field R) by RELAT_1: 15;

      y in ( field R) by A1, RELAT_1: 15;

      hence thesis by A2, ZFMISC_1: 87;

    end;

    

     Lm7: R is reflexive & X c= ( field R) implies ( field (R |_2 X)) = X

    proof

      assume that

       A1: for x be object holds x in ( field R) implies [x, x] in R and

       A2: X c= ( field R);

      thus ( field (R |_2 X)) c= X by WELLORD1: 12;

      let y be object;

      assume

       A3: y in X;

      then

       A4: [y, y] in [:X, X:] by ZFMISC_1: 87;

       [y, y] in R by A1, A2, A3;

      then [y, y] in (R |_2 X) by A4, XBOOLE_0:def 4;

      hence thesis by RELAT_1: 15;

    end;

    theorem :: ORDERS_1:25

    R is being_quasi-order implies (R |_2 X) is being_quasi-order by WELLORD1: 15, WELLORD1: 17;

    theorem :: ORDERS_1:26

    R is being_partial-order implies (R |_2 X) is being_partial-order by WELLORD1: 15, WELLORD1: 17;

    theorem :: ORDERS_1:27

    R is being_linear-order implies (R |_2 X) is being_linear-order by WELLORD1: 15, WELLORD1: 16, WELLORD1: 17;

    registration

      let R be empty Relation;

      cluster ( field R) -> empty;

      coherence ;

    end

    registration

      cluster empty -> being_quasi-order being_partial-order being_linear-order well-ordering for Relation;

      coherence

      proof

        let R be Relation such that

         A1: R is empty;

        thus

         A2: R is reflexive by A1;

        thus

         A3: R is transitive by A1;

        hence R is reflexive & R is transitive by A2;

        thus

         A4: R is antisymmetric by A1;

        hence R is reflexive & R is transitive & R is antisymmetric by A2, A3;

        thus R is connected by A1;

        hence R is reflexive & R is transitive & R is antisymmetric & R is connected by A2, A3, A4;

        let Y;

        assume that

         A5: Y c= ( field R) and

         A6: Y <> {} ;

        thus thesis by A5, A6, A1;

      end;

    end

    registration

      let X;

      cluster ( id X) -> being_quasi-order being_partial-order;

      coherence ;

    end

    definition

      let R, X;

      :: ORDERS_1:def7

      pred R quasi_orders X means R is_reflexive_in X & R is_transitive_in X;

      :: ORDERS_1:def8

      pred R partially_orders X means R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X;

      :: ORDERS_1:def9

      pred R linearly_orders X means R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X;

    end

    theorem :: ORDERS_1:28

    

     Th28: R well_orders X implies R quasi_orders X & R partially_orders X & R linearly_orders X;

    theorem :: ORDERS_1:29

    

     Th29: R linearly_orders X implies R quasi_orders X & R partially_orders X;

    theorem :: ORDERS_1:30

    R partially_orders X implies R quasi_orders X;

    theorem :: ORDERS_1:31

    

     Th31: R is being_quasi-order implies R quasi_orders ( field R)

    proof

      assume that

       A1: R is_reflexive_in ( field R) and

       A2: R is_transitive_in ( field R);

      thus R is_reflexive_in ( field R) & R is_transitive_in ( field R) by A1, A2;

    end;

    theorem :: ORDERS_1:32

    R quasi_orders Y & X c= Y implies R quasi_orders X

    proof

      assume that

       A1: R is_reflexive_in Y and

       A2: R is_transitive_in Y and

       A3: X c= Y;

      thus R is_reflexive_in X & R is_transitive_in X by A1, A2, A3;

    end;

    

     Lm8: R is_reflexive_in X implies (R |_2 X) is reflexive

    proof

      assume

       A1: for x be object holds x in X implies [x, x] in R;

      let x be object;

      assume

       A2: x in ( field (R |_2 X));

      then x in X by WELLORD1: 12;

      then

       A3: [x, x] in [:X, X:] by ZFMISC_1: 87;

       [x, x] in R by A1, A2, WELLORD1: 12;

      hence thesis by A3, XBOOLE_0:def 4;

    end;

    

     Lm9: R is_transitive_in X implies (R |_2 X) is transitive

    proof

      assume

       A1: for x,y,z be object holds x in X & y in X & z in X & [x, y] in R & [y, z] in R implies [x, z] in R;

      let x,y,z be object;

      assume that

       A2: x in ( field (R |_2 X)) and

       A3: y in ( field (R |_2 X)) and

       A4: z in ( field (R |_2 X));

      

       A5: z in X by A4, WELLORD1: 12;

      

       A6: x in X by A2, WELLORD1: 12;

      then

       A7: [x, z] in [:X, X:] by A5, ZFMISC_1: 87;

      assume that

       A8: [x, y] in (R |_2 X) and

       A9: [y, z] in (R |_2 X);

      

       A10: [x, y] in R by A8, XBOOLE_0:def 4;

      

       A11: [y, z] in R by A9, XBOOLE_0:def 4;

      y in X by A3, WELLORD1: 12;

      then [x, z] in R by A1, A6, A5, A10, A11;

      hence thesis by A7, XBOOLE_0:def 4;

    end;

    

     Lm10: R is_antisymmetric_in X implies (R |_2 X) is antisymmetric

    proof

      assume

       A1: for x,y be object holds x in X & y in X & [x, y] in R & [y, x] in R implies x = y;

      let x,y be object;

      assume that

       A2: x in ( field (R |_2 X)) and

       A3: y in ( field (R |_2 X));

      

       A4: y in X by A3, WELLORD1: 12;

      assume that

       A5: [x, y] in (R |_2 X) and

       A6: [y, x] in (R |_2 X);

      

       A7: [x, y] in R by A5, XBOOLE_0:def 4;

      

       A8: [y, x] in R by A6, XBOOLE_0:def 4;

      x in X by A2, WELLORD1: 12;

      hence thesis by A1, A4, A7, A8;

    end;

    

     Lm11: R is_connected_in X implies (R |_2 X) is connected

    proof

      assume

       A1: for x,y be object holds x in X & y in X & x <> y implies [x, y] in R or [y, x] in R;

      let x,y be object;

      assume that

       A2: x in ( field (R |_2 X)) and

       A3: y in ( field (R |_2 X)) and

       A4: x <> y;

      

       A5: y in X by A3, WELLORD1: 12;

      

       A6: x in X by A2, WELLORD1: 12;

      then

       A7: [x, y] in [:X, X:] by A5, ZFMISC_1: 87;

      

       A8: [y, x] in [:X, X:] by A6, A5, ZFMISC_1: 87;

       [x, y] in R or [y, x] in R by A1, A4, A6, A5;

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

    end;

    theorem :: ORDERS_1:33

    R quasi_orders X implies (R |_2 X) is being_quasi-order by Lm8, Lm9;

    theorem :: ORDERS_1:34

    

     Th34: R is being_partial-order implies R partially_orders ( field R)

    proof

      assume that

       A1: R is_reflexive_in ( field R) and

       A2: R is_transitive_in ( field R) and

       A3: R is_antisymmetric_in ( field R);

      thus R is_reflexive_in ( field R) & R is_transitive_in ( field R) & R is_antisymmetric_in ( field R) by A1, A2, A3;

    end;

    theorem :: ORDERS_1:35

    R partially_orders Y & X c= Y implies R partially_orders X

    proof

      assume that

       A1: R is_reflexive_in Y and

       A2: R is_transitive_in Y and

       A3: R is_antisymmetric_in Y and

       A4: X c= Y;

      thus R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X by A1, A2, A3, A4;

    end;

    theorem :: ORDERS_1:36

    R partially_orders X implies (R |_2 X) is being_partial-order by Lm8, Lm9, Lm10;

    theorem :: ORDERS_1:37

    R is being_linear-order implies R linearly_orders ( field R)

    proof

      assume that

       A1: R is_reflexive_in ( field R) and

       A2: R is_transitive_in ( field R) and

       A3: R is_antisymmetric_in ( field R) and

       A4: R is_connected_in ( field R);

      thus R is_reflexive_in ( field R) & R is_transitive_in ( field R) & R is_antisymmetric_in ( field R) & R is_connected_in ( field R) by A1, A2, A3, A4;

    end;

    theorem :: ORDERS_1:38

    R linearly_orders Y & X c= Y implies R linearly_orders X

    proof

      assume that

       A1: R is_reflexive_in Y and

       A2: R is_transitive_in Y and

       A3: R is_antisymmetric_in Y and

       A4: R is_connected_in Y and

       A5: X c= Y;

      thus R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X by A1, A2, A3, A4, A5;

    end;

    theorem :: ORDERS_1:39

    R linearly_orders X implies (R |_2 X) is being_linear-order by Lm8, Lm9, Lm10, Lm11;

    

     Lm12: R is_reflexive_in X implies (R ~ ) is_reflexive_in X

    proof

      assume

       A1: for x be object holds x in X implies [x, x] in R;

      let x be object;

      assume x in X;

      then [x, x] in R by A1;

      hence thesis by RELAT_1:def 7;

    end;

    

     Lm13: R is_transitive_in X implies (R ~ ) is_transitive_in X

    proof

      assume

       A1: for x,y,z be object holds x in X & y in X & z in X & [x, y] in R & [y, z] in R implies [x, z] in R;

      let x,y,z be object;

      assume that

       A2: x in X and

       A3: y in X and

       A4: z in X and

       A5: [x, y] in (R ~ ) and

       A6: [y, z] in (R ~ );

      

       A7: [z, y] in R by A6, RELAT_1:def 7;

       [y, x] in R by A5, RELAT_1:def 7;

      then [z, x] in R by A1, A2, A3, A4, A7;

      hence thesis by RELAT_1:def 7;

    end;

    

     Lm14: R is_antisymmetric_in X implies (R ~ ) is_antisymmetric_in X

    proof

      assume

       A1: for x,y be object holds x in X & y in X & [x, y] in R & [y, x] in R implies x = y;

      let x,y be object;

      assume that

       A2: x in X and

       A3: y in X and

       A4: [x, y] in (R ~ ) and

       A5: [y, x] in (R ~ );

      

       A6: [y, x] in R by A4, RELAT_1:def 7;

       [x, y] in R by A5, RELAT_1:def 7;

      hence thesis by A1, A2, A3, A6;

    end;

    

     Lm15: R is_connected_in X implies (R ~ ) is_connected_in X

    proof

      assume

       A1: for x,y be object holds x in X & y in X & x <> y implies [x, y] in R or [y, x] in R;

      let x,y be object;

      assume that

       A2: x in X and

       A3: y in X and

       A4: x <> y;

       [x, y] in R or [y, x] in R by A1, A2, A3, A4;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: ORDERS_1:40

    R quasi_orders X implies (R ~ ) quasi_orders X by Lm12, Lm13;

    theorem :: ORDERS_1:41

    

     Th41: R partially_orders X implies (R ~ ) partially_orders X by Lm12, Lm13, Lm14;

    theorem :: ORDERS_1:42

    R linearly_orders X implies (R ~ ) linearly_orders X by Lm12, Lm13, Lm14, Lm15;

    theorem :: ORDERS_1:43

    O quasi_orders X

    proof

      

       A1: ( field O) = X by Lm4;

      then

       A2: O is_transitive_in X by RELAT_2:def 16;

      O is_reflexive_in X by A1, RELAT_2:def 9;

      hence thesis by A2;

    end;

    theorem :: ORDERS_1:44

    O partially_orders X

    proof

      

       A1: ( field O) = X by Lm4;

      then

       A2: O is_antisymmetric_in X by RELAT_2:def 12;

      

       A3: O is_transitive_in X by A1, RELAT_2:def 16;

      O is_reflexive_in X by A1, RELAT_2:def 9;

      hence thesis by A2, A3;

    end;

    theorem :: ORDERS_1:45

    

     Th45: R partially_orders X implies (R |_2 X) is Order of X

    proof

      set S = (R |_2 X);

      

       A1: ( field S) c= X by WELLORD1: 13;

      ( rng S) c= ( field S) by XBOOLE_1: 7;

      then

       A2: ( rng S) c= X by A1;

      ( dom S) c= ( field S) by XBOOLE_1: 7;

      then ( dom S) c= X by A1;

      then

      reconsider S as Relation of X by A2, RELSET_1: 4;

      assume

       A3: R partially_orders X;

      

       A4: (R |_2 X) is_antisymmetric_in X

      proof

        

         A5: R is_antisymmetric_in X by A3;

        let x,y be object;

        assume that

         A6: x in X and

         A7: y in X and

         A8: [x, y] in (R |_2 X) and

         A9: [y, x] in (R |_2 X);

        

         A10: [y, x] in R by A9, XBOOLE_0:def 4;

         [x, y] in R by A8, XBOOLE_0:def 4;

        hence thesis by A6, A7, A10, A5;

      end;

      

       A11: (R |_2 X) is_transitive_in X

      proof

        

         A12: R is_transitive_in X by A3;

        let x,y,z be object;

        assume that

         A13: x in X and

         A14: y in X and

         A15: z in X and

         A16: [x, y] in (R |_2 X) and

         A17: [y, z] in (R |_2 X);

        

         A18: [x, z] in [:X, X:] by A13, A15, ZFMISC_1: 87;

        

         A19: [y, z] in R by A17, XBOOLE_0:def 4;

         [x, y] in R by A16, XBOOLE_0:def 4;

        then [x, z] in R by A13, A14, A15, A19, A12;

        hence thesis by A18, XBOOLE_0:def 4;

      end;

      

       A20: R is_reflexive_in X by A3;

      

       A21: (R |_2 X) is_reflexive_in X

      proof

        let x be object;

        assume

         A22: x in X;

        then

         A23: [x, x] in [:X, X:] by ZFMISC_1: 87;

         [x, x] in R by A20, A22;

        hence thesis by A23, XBOOLE_0:def 4;

      end;

      then

       A24: ( field S) = X by Th13;

      ( dom S) = X by A21, Th13;

      hence thesis by A21, A24, A4, A11, PARTFUN1:def 2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16;

    end;

    theorem :: ORDERS_1:46

    R linearly_orders X implies (R |_2 X) is Order of X by Th29, Th45;

    theorem :: ORDERS_1:47

    R well_orders X implies (R |_2 X) is Order of X by Th28, Th45;

    theorem :: ORDERS_1:48

    ( id X) quasi_orders X & ( id X) partially_orders X

    proof

      ( field ( id X)) = (X \/ ( rng ( id X)))

      .= (X \/ X)

      .= X;

      hence thesis by Th31, Th34;

    end;

    definition

      let R, X;

      :: ORDERS_1:def10

      pred X has_upper_Zorn_property_wrt R means for Y st Y c= X & (R |_2 Y) is being_linear-order holds ex x st x in X & for y st y in Y holds [y, x] in R;

      :: ORDERS_1:def11

      pred X has_lower_Zorn_property_wrt R means for Y st Y c= X & (R |_2 Y) is being_linear-order holds ex x st x in X & for y st y in Y holds [x, y] in R;

    end

    

     Lm16: ((R |_2 X) ~ ) = ((R ~ ) |_2 X)

    proof

      now

        let x,y be object;

        thus [x, y] in ((R ~ ) |_2 X) implies [y, x] in (R |_2 X)

        proof

          assume

           A1: [x, y] in ((R ~ ) |_2 X);

          then [x, y] in [:X, X:] by XBOOLE_0:def 4;

          then

           A2: [y, x] in [:X, X:] by ZFMISC_1: 88;

           [x, y] in (R ~ ) by A1, XBOOLE_0:def 4;

          then [y, x] in R by RELAT_1:def 7;

          hence thesis by A2, XBOOLE_0:def 4;

        end;

        assume

         A3: [y, x] in (R |_2 X);

        then [y, x] in [:X, X:] by XBOOLE_0:def 4;

        then

         A4: [x, y] in [:X, X:] by ZFMISC_1: 88;

         [y, x] in R by A3, XBOOLE_0:def 4;

        then [x, y] in (R ~ ) by RELAT_1:def 7;

        hence [x, y] in ((R ~ ) |_2 X) by A4, XBOOLE_0:def 4;

      end;

      hence thesis by RELAT_1:def 7;

    end;

     Lm17:

    now

      let R;

      

      thus (R |_2 {} ) = (( {} |` R) | {} ) by WELLORD1: 10

      .= {} ;

    end;

    theorem :: ORDERS_1:49

    

     Th49: X has_upper_Zorn_property_wrt R implies X <> {}

    proof

      assume

       A1: for Y st Y c= X & (R |_2 Y) is being_linear-order holds ex x st x in X & for y st y in Y holds [y, x] in R;

      (R |_2 {} ) is being_linear-order by Lm17;

      then ex x st x in X & for y st y in {} holds [y, x] in R by A1, XBOOLE_1: 2;

      hence thesis;

    end;

    theorem :: ORDERS_1:50

    X has_lower_Zorn_property_wrt R implies X <> {}

    proof

      assume

       A1: for Y st Y c= X & (R |_2 Y) is being_linear-order holds ex x st x in X & for y st y in Y holds [x, y] in R;

      (R |_2 {} ) is being_linear-order by Lm17;

      then ex x st x in X & for y st y in {} holds [x, y] in R by A1, XBOOLE_1: 2;

      hence thesis;

    end;

    theorem :: ORDERS_1:51

    

     Th51: X has_upper_Zorn_property_wrt R iff X has_lower_Zorn_property_wrt (R ~ )

    proof

      thus X has_upper_Zorn_property_wrt R implies X has_lower_Zorn_property_wrt (R ~ )

      proof

        assume

         A1: for Y st Y c= X & (R |_2 Y) is being_linear-order holds ex x st x in X & for y st y in Y holds [y, x] in R;

        let Y;

        

         A2: (((R |_2 Y) ~ ) ~ ) = (R |_2 Y);

        assume that

         A3: Y c= X and

         A4: ((R ~ ) |_2 Y) is being_linear-order;

        ((R ~ ) |_2 Y) = ((R |_2 Y) ~ ) by Lm16;

        then

        consider x such that

         A5: x in X and

         A6: for y st y in Y holds [y, x] in R by A1, A2, A3, A4, Th18;

        take x;

        thus x in X by A5;

        let y;

        assume y in Y;

        then [y, x] in R by A6;

        hence thesis by RELAT_1:def 7;

      end;

      assume

       A7: for Y st Y c= X & ((R ~ ) |_2 Y) is being_linear-order holds ex x st x in X & for y st y in Y holds [x, y] in (R ~ );

      let Y;

      assume that

       A8: Y c= X and

       A9: (R |_2 Y) is being_linear-order;

      ((R ~ ) |_2 Y) = ((R |_2 Y) ~ ) by Lm16;

      then

      consider x such that

       A10: x in X and

       A11: for y st y in Y holds [x, y] in (R ~ ) by A7, A8, A9, Th18;

      take x;

      thus x in X by A10;

      let y;

      assume y in Y;

      then [x, y] in (R ~ ) by A11;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: ORDERS_1:52

    X has_upper_Zorn_property_wrt (R ~ ) iff X has_lower_Zorn_property_wrt R

    proof

      ((R ~ ) ~ ) = R;

      hence thesis by Th51;

    end;

    definition

      let R, x;

      :: ORDERS_1:def12

      pred x is_maximal_in R means x in ( field R) & not ex y st y in ( field R) & y <> x & [x, y] in R;

      :: ORDERS_1:def13

      pred x is_minimal_in R means x in ( field R) & not ex y st y in ( field R) & y <> x & [y, x] in R;

      :: ORDERS_1:def14

      pred x is_superior_of R means x in ( field R) & for y st y in ( field R) & y <> x holds [y, x] in R;

      :: ORDERS_1:def15

      pred x is_inferior_of R means x in ( field R) & for y st y in ( field R) & y <> x holds [x, y] in R;

    end

    theorem :: ORDERS_1:53

    x is_inferior_of R & R is antisymmetric implies x is_minimal_in R

    proof

      assume that

       A1: x is_inferior_of R and

       A2: R is antisymmetric;

      

       A3: R is_antisymmetric_in ( field R) by A2;

      thus

       A4: x in ( field R) by A1;

      let y;

      assume that

       A5: y in ( field R) and

       A6: y <> x and

       A7: [y, x] in R;

       [x, y] in R by A1, A5, A6;

      hence thesis by A4, A5, A6, A7, A3;

    end;

    theorem :: ORDERS_1:54

    x is_superior_of R & R is antisymmetric implies x is_maximal_in R

    proof

      assume that

       A1: x is_superior_of R and

       A2: R is antisymmetric;

      

       A3: R is_antisymmetric_in ( field R) by A2;

      thus

       A4: x in ( field R) by A1;

      let y;

      assume that

       A5: y in ( field R) and

       A6: y <> x and

       A7: [x, y] in R;

       [y, x] in R by A1, A5, A6;

      hence thesis by A4, A5, A6, A7, A3;

    end;

    theorem :: ORDERS_1:55

    x is_minimal_in R & R is connected implies x is_inferior_of R

    proof

      assume that

       A1: x is_minimal_in R and

       A2: R is connected;

      thus

       A3: x in ( field R) by A1;

      let y;

      assume that

       A4: y in ( field R) and

       A5: y <> x;

      R is_connected_in ( field R) by A2;

      then [x, y] in R or [y, x] in R by A3, A4, A5;

      hence thesis by A1, A4;

    end;

    theorem :: ORDERS_1:56

    x is_maximal_in R & R is connected implies x is_superior_of R

    proof

      assume that

       A1: x is_maximal_in R and

       A2: R is connected;

      thus

       A3: x in ( field R) by A1;

      let y;

      assume that

       A4: y in ( field R) and

       A5: y <> x;

      R is_connected_in ( field R) by A2;

      then [x, y] in R or [y, x] in R by A3, A4, A5;

      hence thesis by A1, A4;

    end;

    theorem :: ORDERS_1:57

    x in X & x is_superior_of R & X c= ( field R) & R is reflexive implies X has_upper_Zorn_property_wrt R

    proof

      assume that

       A1: x in X and

       A2: x is_superior_of R and

       A3: X c= ( field R) and

       A4: R is_reflexive_in ( field R);

      let Y such that

       A5: Y c= X and (R |_2 Y) is being_linear-order;

      take x;

      thus x in X by A1;

      let y;

      assume y in Y;

      then

       A6: y in X by A5;

      y = x or y <> x;

      hence thesis by A2, A3, A4, A6;

    end;

    theorem :: ORDERS_1:58

    x in X & x is_inferior_of R & X c= ( field R) & R is reflexive implies X has_lower_Zorn_property_wrt R

    proof

      assume that

       A1: x in X and

       A2: x is_inferior_of R and

       A3: X c= ( field R) and

       A4: R is_reflexive_in ( field R);

      let Y such that

       A5: Y c= X and (R |_2 Y) is being_linear-order;

      take x;

      thus x in X by A1;

      let y;

      assume y in Y;

      then

       A6: y in X by A5;

      y = x or y <> x;

      hence thesis by A2, A3, A4, A6;

    end;

    theorem :: ORDERS_1:59

    

     Th59: x is_minimal_in R iff x is_maximal_in (R ~ )

    proof

      

       A1: ( field R) = ( field (R ~ )) by RELAT_1: 21;

      thus x is_minimal_in R implies x is_maximal_in (R ~ )

      proof

        assume that

         A2: x in ( field R) and

         A3: not ex y st y in ( field R) & y <> x & [y, x] in R;

        thus x in ( field (R ~ )) by A2, RELAT_1: 21;

        let y;

        assume that

         A4: y in ( field (R ~ )) and

         A5: y <> x;

         not [y, x] in R by A1, A3, A4, A5;

        hence thesis by RELAT_1:def 7;

      end;

      assume that

       A6: x in ( field (R ~ )) and

       A7: not ex y st y in ( field (R ~ )) & y <> x & [x, y] in (R ~ );

      thus x in ( field R) by A6, RELAT_1: 21;

      let y;

      assume that

       A8: y in ( field R) and

       A9: y <> x;

       not [x, y] in (R ~ ) by A1, A7, A8, A9;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: ORDERS_1:60

    x is_minimal_in (R ~ ) iff x is_maximal_in R

    proof

      

       A1: ( field R) = ( field (R ~ )) by RELAT_1: 21;

      thus x is_minimal_in (R ~ ) implies x is_maximal_in R

      proof

        assume that

         A2: x in ( field (R ~ )) and

         A3: not ex y st y in ( field (R ~ )) & y <> x & [y, x] in (R ~ );

        thus x in ( field R) by A2, RELAT_1: 21;

        let y;

        assume that

         A4: y in ( field R) and

         A5: y <> x;

         not [y, x] in (R ~ ) by A1, A3, A4, A5;

        hence thesis by RELAT_1:def 7;

      end;

      assume that

       A6: x in ( field R) and

       A7: not ex y st y in ( field R) & y <> x & [x, y] in R;

      thus x in ( field (R ~ )) by A6, RELAT_1: 21;

      let y;

      assume that

       A8: y in ( field (R ~ )) and

       A9: y <> x;

       not [x, y] in R by A1, A7, A8, A9;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: ORDERS_1:61

    x is_inferior_of R iff x is_superior_of (R ~ )

    proof

      

       A1: ( field R) = ( field (R ~ )) by RELAT_1: 21;

      thus x is_inferior_of R implies x is_superior_of (R ~ )

      proof

        assume that

         A2: x in ( field R) and

         A3: for y st y in ( field R) & y <> x holds [x, y] in R;

        thus x in ( field (R ~ )) by A2, RELAT_1: 21;

        let y;

        assume that

         A4: y in ( field (R ~ )) and

         A5: y <> x;

         [x, y] in R by A1, A3, A4, A5;

        hence thesis by RELAT_1:def 7;

      end;

      assume that

       A6: x in ( field (R ~ )) and

       A7: for y st y in ( field (R ~ )) & y <> x holds [y, x] in (R ~ );

      thus x in ( field R) by A6, RELAT_1: 21;

      let y;

      assume that

       A8: y in ( field R) and

       A9: y <> x;

       [y, x] in (R ~ ) by A1, A7, A8, A9;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: ORDERS_1:62

    x is_inferior_of (R ~ ) iff x is_superior_of R

    proof

      

       A1: ( field R) = ( field (R ~ )) by RELAT_1: 21;

      thus x is_inferior_of (R ~ ) implies x is_superior_of R

      proof

        assume that

         A2: x in ( field (R ~ )) and

         A3: for y st y in ( field (R ~ )) & y <> x holds [x, y] in (R ~ );

        thus x in ( field R) by A2, RELAT_1: 21;

        let y;

        assume that

         A4: y in ( field R) and

         A5: y <> x;

         [x, y] in (R ~ ) by A1, A3, A4, A5;

        hence thesis by RELAT_1:def 7;

      end;

      assume that

       A6: x in ( field R) and

       A7: for y st y in ( field R) & y <> x holds [y, x] in R;

      thus x in ( field (R ~ )) by A6, RELAT_1: 21;

      let y;

      assume that

       A8: y in ( field (R ~ )) and

       A9: y <> x;

       [y, x] in R by A1, A7, A8, A9;

      hence thesis by RELAT_1:def 7;

    end;

    

     Lm18: 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_transitive_in X by A1;

      

       A4: R is_connected_in X by A1;

      

       A5: R is_antisymmetric_in X by A1;

      

       A6: R is_well_founded_in X by A1;

      R is_reflexive_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, A5, A4;

      let Z;

      assume that

       A7: Z c= Y and

       A8: Z <> {} ;

      Z c= X by A2, A7;

      hence thesis by A8, A6;

    end;

    reserve A,C for Ordinal;

    theorem :: ORDERS_1:63

    

     Th63: for R, X st R partially_orders X & ( field R) = X & X has_upper_Zorn_property_wrt R holds ex x st x is_maximal_in R

    proof

      let R;

      let FIELD be set;

      assume that

       A1: R is_reflexive_in FIELD and

       A2: R is_transitive_in FIELD and

       A3: R is_antisymmetric_in FIELD and

       A4: ( field R) = FIELD and

       A5: FIELD has_upper_Zorn_property_wrt R;

      reconsider XD = FIELD as non empty set by A5, Th49;

      consider D such that

       A6: D = XD;

      

       A7: D in ( bool D) by ZFMISC_1:def 1;

       not D in { {} } by TARSKI:def 1;

      then

      reconsider M = (( bool D) \ { {} }) as non empty set by A7, XBOOLE_0:def 5;

      set f = the Choice_Function of M;

      defpred P[ object, object] means $1 <> {} & $2 = (f . $1) or $1 = {} & $2 = D;

      

       A8: for x be object st x in ( bool D) holds ex y be object st P[x, y]

      proof

        let x be object such that x in ( bool D);

        x = {} implies thesis;

        hence thesis;

      end;

      

       A9: for x,y,z be object st x in ( bool D) & P[x, y] & P[x, z] holds y = z;

      consider g such that

       A10: ( dom g) = ( bool D) & for x be object st x in ( bool D) holds P[x, (g . x)] from FUNCT_1:sch 2( A9, A8);

      defpred ON[ Ordinal, object] means ex L st $2 = (g . { d : for x st x in ( rng L) holds x <> d & [x, d] in R }) & ( dom L) = $1 & for A, L1 st A in $1 & L1 = (L | A) holds (L . A) = (g . { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R });

      

       A11: ON[A, x] & ON[A, y] implies x = y

      proof

        given L1 such that

         A12: x = (g . { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R }) and

         A13: ( dom L1) = A & for C, L st C in A & L = (L1 | C) holds (L1 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R });

        

         A14: L1 = (L1 | A) by A13;

        given L2 such that

         A15: y = (g . { d1 : for x st x in ( rng L2) holds x <> d1 & [x, d1] in R }) and

         A16: ( dom L2) = A & for C, L st C in A & L = (L2 | C) holds (L2 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R });

        defpred P[ Ordinal] means $1 c= A implies (L1 | $1) = (L2 | $1);

        

         A17: for A1 st for A2 st A2 in A1 holds P[A2] holds P[A1]

        proof

          let A1 such that

           A18: for A2 st A2 in A1 holds A2 c= A implies (L1 | A2) = (L2 | A2) and

           A19: A1 c= A;

          

           A20: ( dom (L2 | A1)) = A1 by A16, A19, RELAT_1: 62;

           A21:

          now

            let x be object;

            assume

             A22: x in A1;

            then

            reconsider A3 = x as Ordinal;

            

             A23: (L1 . x) = ((L1 | A1) . x) by A22, FUNCT_1: 49;

            A3 c= A by A19, A22, ORDINAL1:def 2;

            then

             A24: (L1 | A3) = (L2 | A3) by A18, A22;

            

             A25: (L2 . A3) = (g . { d2 : for x st x in ( rng (L2 | A3)) holds x <> d2 & [x, d2] in R }) by A16, A19, A22;

            (L1 . A3) = (g . { d1 : for x st x in ( rng (L1 | A3)) holds x <> d1 & [x, d1] in R }) by A13, A19, A22;

            hence ((L1 | A1) . x) = ((L2 | A1) . x) by A22, A24, A23, A25, FUNCT_1: 49;

          end;

          ( dom (L1 | A1)) = A1 by A13, A19, RELAT_1: 62;

          hence thesis by A20, A21, FUNCT_1: 2;

        end;

        for A1 holds P[A1] from ORDINAL1:sch 2( A17);

        then

         A26: (L1 | A) = (L2 | A);

        L2 = (L2 | A) by A16;

        hence thesis by A12, A15, A26, A14;

      end;

       {} in { {} } by TARSKI:def 1;

      then

       A27: not {} in M by XBOOLE_0:def 5;

      

       A28: X in ( bool D) & X <> {} implies (g . X) in X

      proof

        assume that

         A29: X in ( bool D) and

         A30: X <> {} ;

         not X in { {} } by A30, TARSKI:def 1;

        then

         A31: X in M by A29, XBOOLE_0:def 5;

        (f . X) = (g . X) by A10, A29, A30;

        hence thesis by A27, A31, Lm2;

      end;

      defpred OM[ Ordinal] means ON[$1, D];

       {} c= D;

      then

       A32: (g . {} ) = D by A10;

       A33:

      now

        let A, B, L1, L2;

        assume that

         A34: ( dom L1) = A & for C, L st C in A & L = (L1 | C) holds (L1 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R }) and

         A35: ( dom L2) = B & for C, L st C in B & L = (L2 | C) holds (L2 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R });

        let C such that

         A36: C c= A and

         A37: C c= B;

        defpred P[ Ordinal] means $1 c= C implies (L1 | $1) = (L2 | $1);

        

         A38: for A1 st for A2 st A2 in A1 holds P[A2] holds P[A1]

        proof

          let A1 such that

           A39: for A2 st A2 in A1 holds A2 c= C implies (L1 | A2) = (L2 | A2) and

           A40: A1 c= C;

          

           A41: ( dom (L2 | A1)) = A1 by A35, A37, A40, RELAT_1: 62, XBOOLE_1: 1;

           A42:

          now

            let x be object;

            assume

             A43: x in A1;

            then

            reconsider A3 = x as Ordinal;

            

             A44: (L1 . x) = ((L1 | A1) . x) by A43, FUNCT_1: 49;

            A3 c= C by A40, A43, ORDINAL1:def 2;

            then

             A45: (L1 | A3) = (L2 | A3) by A39, A43;

            

             A46: A3 in C by A40, A43;

            then

             A47: (L2 . A3) = (g . { d2 : for x st x in ( rng (L2 | A3)) holds x <> d2 & [x, d2] in R }) by A35, A37;

            (L1 . A3) = (g . { d1 : for x st x in ( rng (L1 | A3)) holds x <> d1 & [x, d1] in R }) by A34, A36, A46;

            hence ((L1 | A1) . x) = ((L2 | A1) . x) by A43, A45, A44, A47, FUNCT_1: 49;

          end;

          ( dom (L1 | A1)) = A1 by A34, A36, A40, RELAT_1: 62, XBOOLE_1: 1;

          hence thesis by A41, A42, FUNCT_1: 2;

        end;

        for A1 holds P[A1] from ORDINAL1:sch 2( A38);

        hence (L1 | C) = (L2 | C);

      end;

      

       A48: for d, A, B st ON[A, d] & ON[B, d] holds A = B

      proof

        let d, A, B;

        given L1 such that

         A49: d = (g . { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R }) and

         A50: ( dom L1) = A & for C, L st C in A & L = (L1 | C) holds (L1 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R });

        given L2 such that

         A51: d = (g . { d1 : for x st x in ( rng L2) holds x <> d1 & [x, d1] in R }) and

         A52: ( dom L2) = B & for C, L st C in B & L = (L2 | C) holds (L2 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R });

         A53:

        now

          set Y = { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R };

          set X = { d1 : for x st x in ( rng (L1 | B)) holds x <> d1 & [x, d1] in R };

          

           A54: Y c= D

          proof

            let x be object;

            assume x in Y;

            then ex d1 st x = d1 & for x st x in ( rng L1) holds x <> d1 & [x, d1] in R;

            hence thesis;

          end;

          assume

           A55: B in A;

          then B c= A by ORDINAL1:def 2;

          

          then

           A56: (L1 | B) = (L2 | B) by A33, A50, A52

          .= L2 by A52;

          (L1 . B) = (g . X) by A50, A55;

          then

           A57: d in ( rng L1) by A50, A51, A55, A56, FUNCT_1:def 3;

           A58:

          now

            assume

             A59: Y <> {} ;

            then not Y in { {} } by TARSKI:def 1;

            then

             A60: Y in M by A54, XBOOLE_0:def 5;

            (g . Y) = (f . Y) by A10, A54, A59;

            then d in Y by A27, A49, A60, Lm2;

            then ex d1 st d = d1 & for x st x in ( rng L1) holds x <> d1 & [x, d1] in R;

            hence contradiction by A57;

          end;

          

           A61: not d in d;

           P[Y, (g . Y)] by A10, A54;

          hence contradiction by A49, A61, A58;

        end;

        now

          set Y = { d1 : for x st x in ( rng L2) holds x <> d1 & [x, d1] in R };

          set X = { d1 : for x st x in ( rng (L2 | A)) holds x <> d1 & [x, d1] in R };

          

           A62: Y c= D

          proof

            let x be object;

            assume x in Y;

            then ex d1 st x = d1 & for x st x in ( rng L2) holds x <> d1 & [x, d1] in R;

            hence thesis;

          end;

          assume

           A63: A in B;

          then A c= B by ORDINAL1:def 2;

          

          then

           A64: (L2 | A) = (L1 | A) by A33, A50, A52

          .= L1 by A50;

          (L2 . A) = (g . X) by A52, A63;

          then

           A65: d in ( rng L2) by A49, A52, A63, A64, FUNCT_1:def 3;

           A66:

          now

            assume

             A67: Y <> {} ;

            then not Y in { {} } by TARSKI:def 1;

            then

             A68: Y in M by A62, XBOOLE_0:def 5;

            (g . Y) = (f . Y) by A10, A62, A67;

            then d in Y by A27, A51, A68, Lm2;

            then ex d1 st d = d1 & for x st x in ( rng L2) holds x <> d1 & [x, d1] in R;

            hence contradiction by A65;

          end;

          

           A69: not d in d;

           P[Y, (g . Y)] by A10, A62;

          hence contradiction by A51, A69, A66;

        end;

        hence thesis by A53, ORDINAL1: 14;

      end;

      

       A70: ex A1 st OM[A1]

      proof

        defpred P[ object, object] means ex A st $2 = A & ON[A, $1];

        defpred OO[ Ordinal] means ex d st ON[$1, d];

        assume

         A71: for A1 holds not ON[A1, D];

        

         A72: for A st for B st B in A holds OO[B] holds OO[A]

        proof

          defpred P[ object, object] means ex C st $1 = C & ON[C, $2];

          let A such that

           A73: for B st B in A holds ex d st ON[B, d];

          

           A74: for x be object st x in A holds ex y be object st P[x, y]

          proof

            let x be object;

            assume

             A75: x in A;

            then

            reconsider C = x as Ordinal;

            consider d such that

             A76: ON[C, d] by A73, A75;

            reconsider y = d as set;

            take y, C;

            thus thesis by A76;

          end;

          

           A77: for x,y,z be object st x in A & P[x, y] & P[x, z] holds y = z by A11;

          consider h such that

           A78: ( dom h) = A & for x be object st x in A holds P[x, (h . x)] from FUNCT_1:sch 2( A77, A74);

          reconsider h as Sequence by A78, ORDINAL1:def 7;

          set X = { d1 : for x st x in ( rng h) holds x <> d1 & [x, d1] in R };

          

           A79: X c= D

          proof

            let x be object;

            assume x in X;

            then ex d1 st x = d1 & for x st x in ( rng h) holds x <> d1 & [x, d1] in R;

            hence thesis;

          end;

          

           A80: ON[A, (g . X)]

          proof

            take h;

            thus (g . X) = (g . { d1 : for x st x in ( rng h) holds x <> d1 & [x, d1] in R }) & ( dom h) = A by A78;

            let B, L;

            assume that

             A81: B in A and

             A82: L = (h | B);

            ex C st B = C & ON[C, (h . B)] by A78, A81;

            then

            consider L1 such that

             A83: (h . B) = (g . { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R }) and

             A84: ( dom L1) = B & for C, L st C in B & L = (L1 | C) holds (L1 . C) = (g . { d1 : for x st x in ( rng L) holds x <> d1 & [x, d1] in R });

            

             A85: for x be object st x in B holds (L1 . x) = ((h | B) . x)

            proof

              let x be object;

              assume

               A86: x in B;

              then

              reconsider A1 = x as Ordinal;

              

               A87: ((h | B) . x) = (h . x) by A86, FUNCT_1: 49;

              

               A88: ON[A1, (L1 . x)]

              proof

                reconsider K = (L1 | A1) as Sequence;

                take K;

                thus (L1 . x) = (g . { d1 : for x st x in ( rng K) holds x <> d1 & [x, d1] in R }) by A84, A86;

                A1 c= B by A86, ORDINAL1:def 2;

                hence ( dom K) = A1 by A84, RELAT_1: 62;

                let A2, L2;

                assume that

                 A89: A2 in A1 and

                 A90: L2 = (K | A2);

                A2 c= A1 by A89, ORDINAL1:def 2;

                then

                 A91: L2 = (L1 | A2) by A90, FUNCT_1: 51;

                (K . A2) = (L1 . A2) by A89, FUNCT_1: 49;

                hence thesis by A84, A86, A89, A91, ORDINAL1: 10;

              end;

              ex A2 st x = A2 & ON[A2, (h . x)] by A78, A81, A86, ORDINAL1: 10;

              hence thesis by A11, A88, A87;

            end;

            B c= A by A81, ORDINAL1:def 2;

            then ( dom (h | B)) = B by A78, RELAT_1: 62;

            then (h | B) = L1 by A84, A85, FUNCT_1: 2;

            hence thesis by A82, A83;

          end;

          then X <> {} by A32, A71;

          then (g . X) in X by A28, A79;

          then

          reconsider dd = (g . X) as Element of D by A79;

          take dd;

          thus thesis by A80;

        end;

        

         A92: for A holds OO[A] from ORDINAL1:sch 2( A72);

        

         A93: for x,y,z be object st P[x, y] & P[x, z] holds y = z

        proof

          let x,y,z be object;

          given A1 such that

           A94: y = A1 and

           A95: ON[A1, x];

          consider d1 such that

           A96: ON[A1, d1] by A92;

          given A2 such that

           A97: z = A2 and

           A98: ON[A2, x];

          d1 = x by A11, A95, A96;

          hence thesis by A48, A94, A95, A97, A98;

        end;

        consider X such that

         A99: for x be object holds x in X iff ex y be object st y in D & P[y, x] from TARSKI:sch 1( A93);

        for A holds A in X

        proof

          let A;

          ex d st ON[A, d] by A92;

          hence thesis by A99;

        end;

        hence contradiction by ORDINAL1: 26;

      end;

      consider A such that

       A100: OM[A] & for B st OM[B] holds A c= B from ORDINAL1:sch 1( A70);

      

       A101: for L holds { d : for x st x in ( rng L) holds x <> d & [x, d] in R } c= D

      proof

        let L;

        let x be object;

        assume x in { d : for x st x in ( rng L) holds x <> d & [x, d] in R };

        then ex d1 st x = d1 & for x st x in ( rng L) holds x <> d1 & [x, d1] in R;

        hence thesis;

      end;

      D in ( bool D) by ZFMISC_1:def 1;

      then

      reconsider d = (g . D) as Element of D by A28;

      

       A102: d in D & ON[ {} , d]

      proof

        deffunc H( set) = {} ;

        thus d in D;

        consider L such that

         A103: ( dom L) = {} & for B, L1 st B in {} & L1 = (L | B) holds (L . B) = H(L1) from ORDINAL1:sch 4;

        take L;

        

         A104: D c= { d1 : for x st x in ( rng L) holds x <> d1 & [x, d1] in R }

        proof

          let x be object;

          assume x in D;

          then

          reconsider d = x as Element of D;

          for x st x in ( rng L) holds x <> d & [x, d] in R by A103, RELAT_1: 42;

          hence thesis;

        end;

        { d1 : for x st x in ( rng L) holds x <> d1 & [x, d1] in R } c= D by A101;

        hence d = (g . { d1 : for x st x in ( rng L) holds x <> d1 & [x, d1] in R }) by A104, XBOOLE_0:def 10;

        thus ( dom L) = {} by A103;

        thus thesis;

      end;

      

       A105: {} c= A;

      defpred P[ object] means ex B st B in A & ON[B, $1];

      consider X such that

       A106: for x be object holds x in X iff x in D & P[x] from XBOOLE_0:sch 1;

       not Y in Y;

      then d <> D;

      then {} <> A by A11, A100, A102;

      then {} c< A by A105;

      then {} in A by ORDINAL1: 11;

      then

      reconsider X as non empty set by A106, A102;

      consider L such that

       A107: D = (g . { d1 : for x st x in ( rng L) holds x <> d1 & [x, d1] in R }) and

       A108: ( dom L) = A & for B, L1 st B in A & L1 = (L | B) holds (L . B) = (g . { d2 : for x st x in ( rng L1) holds x <> d2 & [x, d2] in R }) by A100;

      R is transitive by A2, A4;

      then

       A109: (R |_2 X) is transitive by WELLORD1: 17;

      

       A110: ( rng L) c= X

      proof

        let z be object;

        assume z in ( rng L);

        then

        consider y be object such that

         A111: y in ( dom L) and

         A112: z = (L . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A111;

        set Z = { d2 : for x st x in ( rng (L | y)) holds x <> d2 & [x, d2] in R };

        

         A113: Z c= D by A101;

        

         A114: ON[y, z]

        proof

          reconsider K = (L | y) as Sequence;

          take K;

          thus z = (g . { d2 : for x st x in ( rng K) holds x <> d2 & [x, d2] in R }) by A108, A111, A112;

          y c= ( dom L) by A111, ORDINAL1:def 2;

          hence

           A115: ( dom K) = y by RELAT_1: 62;

          let B, L1;

          assume that

           A116: B in y and

           A117: L1 = (K | B);

          B c= y by A116, ORDINAL1:def 2;

          then

           A118: L1 = (L | B) by A117, FUNCT_1: 51;

          (K . B) = (L . B) by A115, A116, FUNCT_1: 47;

          hence thesis by A108, A111, A116, A118, ORDINAL1: 10;

        end;

        now

          assume Z = {} ;

          then z = D by A32, A108, A111, A112;

          then ( dom L) c= y by A100, A108, A114;

          hence contradiction by A111, ORDINAL1: 5;

        end;

        then (g . Z) in Z by A28, A113;

        then z in Z by A108, A111, A112;

        hence thesis by A106, A108, A111, A114, A113;

      end;

      

       A119: (R |_2 X) is connected

      proof

        let x,y be object;

        assume that

         A120: x in ( field (R |_2 X)) and

         A121: y in ( field (R |_2 X));

        

         A122: x in X by A120, WELLORD1: 12;

        then

        consider A1 such that A1 in A and

         A123: ON[A1, x] by A106;

        

         A124: y in X by A121, WELLORD1: 12;

        then

        consider A2 such that A2 in A and

         A125: ON[A2, y] by A106;

        reconsider x9 = x, y9 = y as Element of D by A106, A122, A124;

        consider L1 such that

         A126: x9 = (g . { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R }) and

         A127: ( dom L1) = A1 & for C, L st C in A1 & L = (L1 | C) holds (L1 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R }) by A123;

        consider L2 such that

         A128: y9 = (g . { d1 : for x st x in ( rng L2) holds x <> d1 & [x, d1] in R }) and

         A129: ( dom L2) = A2 & for C, L st C in A2 & L = (L2 | C) holds (L2 . C) = (g . { d2 : for x st x in ( rng L) holds x <> d2 & [x, d2] in R }) by A125;

        

         A130: [x, y] in [:X, X:] by A122, A124, ZFMISC_1: 87;

         A131:

        now

          set Y = { d1 : for x st x in ( rng L2) holds x <> d1 & [x, d1] in R };

          set Z = { d1 : for x st x in ( rng (L2 | A1)) holds x <> d1 & [x, d1] in R };

           not y9 in y9;

          then

           A132: Y <> {} by A32, A128;

          Y c= D by A101;

          then y9 in Y by A28, A128, A132;

          then

           A133: ex d1 st y9 = d1 & for x st x in ( rng L2) holds x <> d1 & [x, d1] in R;

          assume

           A134: A1 in A2;

          then A1 c= A2 by ORDINAL1:def 2;

          

          then

           A135: (L2 | A1) = (L1 | A1) by A33, A127, A129

          .= L1 by A127;

          (L2 . A1) = (g . Z) by A129, A134;

          then x9 in ( rng L2) by A126, A129, A134, A135, FUNCT_1:def 3;

          then [x, y] in R by A133;

          hence thesis by A130, XBOOLE_0:def 4;

        end;

        

         A136: [y, x] in [:X, X:] by A122, A124, ZFMISC_1: 87;

         A137:

        now

          set Y = { d1 : for x st x in ( rng L1) holds x <> d1 & [x, d1] in R };

          set Z = { d1 : for x st x in ( rng (L1 | A2)) holds x <> d1 & [x, d1] in R };

           not d1 in d1;

          then

           A138: Y <> {} by A32, A126;

          Y c= D by A101;

          then x9 in Y by A28, A126, A138;

          then

           A139: ex d1 st x9 = d1 & for x st x in ( rng L1) holds x <> d1 & [x, d1] in R;

          assume

           A140: A2 in A1;

          then A2 c= A1 by ORDINAL1:def 2;

          

          then

           A141: (L1 | A2) = (L2 | A2) by A33, A127, A129

          .= L2 by A129;

          (L1 . A2) = (g . Z) by A127, A140;

          then y9 in ( rng L1) by A127, A128, A140, A141, FUNCT_1:def 3;

          then [y, x] in R by A139;

          hence thesis by A136, XBOOLE_0:def 4;

        end;

        A1 = A2 implies thesis by A11, A123, A125;

        hence thesis by A131, A137, ORDINAL1: 14;

      end;

      R is antisymmetric by A3, A4;

      then

       A142: (R |_2 X) is antisymmetric;

      set Z = { d1 : for x st x in ( rng L) holds x <> d1 & [x, d1] in R };

      

       A143: X c= D by A106;

      R is reflexive by A1, A4;

      then (R |_2 X) is reflexive by WELLORD1: 15;

      then (R |_2 X) is being_linear-order by A109, A142, A119;

      then

      consider x such that

       A144: x in D and

       A145: for y st y in X holds [y, x] in R by A5, A6, A143;

      take x;

      thus x in ( field R) by A4, A6, A144;

      let y such that

       A146: y in ( field R) and

       A147: y <> x and

       A148: [x, y] in R;

      reconsider y9 = y as Element of D by A4, A6, A146;

       A149:

      now

        assume y in X;

        then [y, x] in R by A145;

        hence contradiction by A3, A4, A6, A144, A146, A147, A148;

      end;

      now

        let z;

        assume

         A150: z in ( rng L);

        then

        reconsider z9 = z as Element of X by A110;

        thus z <> y9 by A110, A149, A150;

        

         A151: [z9, x] in R by A145;

        z in D by A106, A110, A150;

        hence [z, y] in R by A2, A4, A6, A144, A146, A148, A151;

      end;

      then

       A152: y in Z;

      Z c= D by A101;

      hence contradiction by A28, A107, A152, ORDINAL1: 5;

    end;

    theorem :: ORDERS_1:64

    

     Th64: for R, X st R partially_orders X & ( field R) = X & X has_lower_Zorn_property_wrt R holds ex x st x is_minimal_in R

    proof

      let R, X such that

       A1: R partially_orders X and

       A2: ( field R) = X and

       A3: X has_lower_Zorn_property_wrt R;

      R = ((R ~ ) ~ );

      then

       A4: X has_upper_Zorn_property_wrt (R ~ ) by A3, Th51;

      ( field (R ~ )) = X by A2, RELAT_1: 21;

      then

      consider x such that

       A5: x is_maximal_in (R ~ ) by A1, A4, Th41, Th63;

      take x;

      thus thesis by A5, Th59;

    end;

    ::$Notion-Name

    ::$Notion-Name

    theorem :: ORDERS_1:65

    

     Th65: for X st X <> {} & for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y holds ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z

    proof

      let X;

      assume that

       A1: X <> {} and

       A2: for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y;

      reconsider D = X as non empty set by A1;

      set R = ( RelIncl D);

      

       A3: D has_upper_Zorn_property_wrt R

      proof

        let Z;

        assume that

         A4: Z c= D and

         A5: (R |_2 Z) is being_linear-order;

        set Q = (R |_2 Z);

        

         A6: Z c= ( field (R |_2 Z))

        proof

          let x be object;

          assume

           A7: x in Z;

          then

           A8: [x, x] in [:Z, Z:] by ZFMISC_1: 87;

           [x, x] in R by A4, A7, WELLORD2:def 1;

          then [x, x] in (R |_2 Z) by A8, XBOOLE_0:def 4;

          hence thesis by RELAT_1: 15;

        end;

        (R |_2 Z) is connected by A5;

        then

         A9: (R |_2 Z) is_connected_in ( field (R |_2 Z));

        Z is c=-linear

        proof

          let X1, X2;

          assume that

           A10: X1 in Z and

           A11: X2 in Z;

          X1 <> X2 implies [X1, X2] in Q or [X2, X1] in Q by A9, A6, A10, A11;

          then X1 <> X2 implies [X1, X2] in R or [X2, X1] in R by XBOOLE_0:def 4;

          hence X1 c= X2 or X2 c= X1 by A4, A10, A11, WELLORD2:def 1;

        end;

        then

        consider Y such that

         A12: Y in X and

         A13: for X1 st X1 in Z holds X1 c= Y by A2, A4;

        take x = Y;

        thus x in D by A12;

        let y;

        assume

         A14: y in Z;

        then y c= Y by A13;

        hence thesis by A4, A12, A14, WELLORD2:def 1;

      end;

      

       A15: ( field R) = D by WELLORD2:def 1;

      

       A16: R is_antisymmetric_in D by A15, RELAT_2:def 12;

      

       A17: R is_transitive_in D by A15, RELAT_2:def 16;

      R is_reflexive_in D by A15, RELAT_2:def 9;

      then R partially_orders D by A17, A16;

      then

      consider x such that

       A18: x is_maximal_in R by A15, A3, Th63;

      take Y = x;

      

       A19: Y in ( field R) by A18;

      thus Y in X by A15, A18;

      let Z;

      assume that

       A20: Z in X and

       A21: Z <> Y;

       not [Y, Z] in R by A15, A18, A20, A21;

      hence thesis by A15, A19, A20, WELLORD2:def 1;

    end;

    theorem :: ORDERS_1:66

    

     Th66: for X st X <> {} & for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds Y c= X1 holds ex Y st Y in X & for Z st Z in X & Z <> Y holds not Z c= Y

    proof

      let X;

      assume that

       A1: X <> {} and

       A2: for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds Y c= X1;

      reconsider D = X as non empty set by A1;

      set R = (( RelIncl D) ~ );

      

       A3: x in D implies [x, x] in R

      proof

        x in D implies [x, x] in ( RelIncl D) by WELLORD2:def 1;

        hence thesis by RELAT_1:def 7;

      end;

      

       A4: D has_upper_Zorn_property_wrt R

      proof

        let Z;

        assume that

         A5: Z c= D and

         A6: (R |_2 Z) is being_linear-order;

        set Q = (R |_2 Z);

        

         A7: Z c= ( field (R |_2 Z))

        proof

          let x be object;

          assume

           A8: x in Z;

          then

           A9: [x, x] in [:Z, Z:] by ZFMISC_1: 87;

           [x, x] in R by A3, A5, A8;

          then [x, x] in (R |_2 Z) by A9, XBOOLE_0:def 4;

          hence thesis by RELAT_1: 15;

        end;

        (R |_2 Z) is connected by A6;

        then

         A10: (R |_2 Z) is_connected_in ( field (R |_2 Z));

        Z is c=-linear

        proof

          let X1, X2;

          assume that

           A11: X1 in Z and

           A12: X2 in Z;

          X1 <> X2 implies [X1, X2] in Q or [X2, X1] in Q by A10, A7, A11, A12;

          then X1 <> X2 implies [X1, X2] in R or [X2, X1] in R by XBOOLE_0:def 4;

          then X1 <> X2 implies [X1, X2] in ( RelIncl D) or [X2, X1] in ( RelIncl D) by RELAT_1:def 7;

          hence X1 c= X2 or X2 c= X1 by A5, A11, A12, WELLORD2:def 1;

        end;

        then

        consider Y such that

         A13: Y in X and

         A14: for X1 st X1 in Z holds Y c= X1 by A2, A5;

        take x = Y;

        thus x in D by A13;

        let y;

        assume

         A15: y in Z;

        then Y c= y by A14;

        then [Y, y] in ( RelIncl D) by A5, A13, A15, WELLORD2:def 1;

        hence thesis by RELAT_1:def 7;

      end;

      

       A16: ( field R) = ( field ( RelIncl D)) by RELAT_1: 21

      .= D by WELLORD2:def 1;

      

       A17: ( field ( RelIncl D)) = D by WELLORD2:def 1;

      ( RelIncl D) is_antisymmetric_in D by A17, RELAT_2:def 12;

      then

       A18: R is_antisymmetric_in D by Lm14;

      ( RelIncl D) is_transitive_in D by A17, RELAT_2:def 16;

      then

       A19: R is_transitive_in D by Lm13;

      ( RelIncl D) is_reflexive_in D by A17, RELAT_2:def 9;

      then R is_reflexive_in D by Lm12;

      then R partially_orders D by A19, A18;

      then

      consider x such that

       A20: x is_maximal_in R by A16, A4, Th63;

      take Y = x;

      

       A21: Y in ( field R) by A20;

      thus Y in X by A16, A20;

      let Z;

      assume that

       A22: Z in X and

       A23: Z <> Y;

       not [Y, Z] in R by A16, A20, A22, A23;

      then not [Z, Y] in ( RelIncl D) by RELAT_1:def 7;

      hence thesis by A16, A21, A22, WELLORD2:def 1;

    end;

    theorem :: ORDERS_1:67

    

     Th67: for X st X <> {} & for Z st Z <> {} & Z c= X & Z is c=-linear holds ( union Z) in X holds ex Y st Y in X & for Z st Z in X & Z <> Y holds not Y c= Z

    proof

      let X such that

       A1: X <> {} and

       A2: for Z st Z <> {} & Z c= X & Z is c=-linear holds ( union Z) in X;

      for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds X1 c= Y

      proof

        set x = the Element of X;

        let Z such that

         A3: Z c= X and

         A4: Z is c=-linear;

        Z <> {} or Z = {} ;

        then

        consider Y such that

         A5: Y = ( union Z) & Z <> {} or Y = x & Z = {} ;

        take Y;

        thus thesis by A1, A2, A3, A4, A5, ZFMISC_1: 74;

      end;

      hence thesis by A1, Th65;

    end;

    theorem :: ORDERS_1:68

    for X st X <> {} & for Z st Z <> {} & Z c= X & Z is c=-linear holds ( meet Z) in X holds ex Y st Y in X & for Z st Z in X & Z <> Y holds not Z c= Y

    proof

      let X such that

       A1: X <> {} and

       A2: for Z st Z <> {} & Z c= X & Z is c=-linear holds ( meet Z) in X;

      for Z st Z c= X & Z is c=-linear holds ex Y st Y in X & for X1 st X1 in Z holds Y c= X1

      proof

        set x = the Element of X;

        let Z such that

         A3: Z c= X and

         A4: Z is c=-linear;

        Z <> {} or Z = {} ;

        then

        consider Y such that

         A5: Y = ( meet Z) & Z <> {} or Y = x & Z = {} ;

        take Y;

        thus thesis by A1, A2, A3, A4, A5, SETFAM_1: 3;

      end;

      hence thesis by A1, Th66;

    end;

    scheme :: ORDERS_1:sch1

    ZornMax { A() -> non empty set , P[ set, set] } :

ex x be Element of A() st for y be Element of A() st x <> y holds not P[x, y]

      provided

       A1: for x be Element of A() holds P[x, x]

       and

       A2: for x,y be Element of A() st P[x, y] & P[y, x] holds x = y

       and

       A3: for x,y,z be Element of A() st P[x, y] & P[y, z] holds P[x, z]

       and

       A4: for X st X c= A() & (for x,y be Element of A() st x in X & y in X holds P[x, y] or P[y, x]) holds ex y be Element of A() st for x be Element of A() st x in X holds P[x, y];

      consider R be Relation of A() such that

       A5: for x,y be Element of A() holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

      

       A6: R is_transitive_in A()

      proof

        let x,y,z be object;

        assume that

         A7: x in A() and

         A8: y in A() and

         A9: z in A();

        reconsider x9 = x, y9 = y, z9 = z as Element of A() by A7, A8, A9;

        assume that

         A10: [x, y] in R and

         A11: [y, z] in R;

        

         A12: P[y9, z9] by A5, A11;

        P[x9, y9] by A5, A10;

        then P[x9, z9] by A3, A12;

        hence thesis by A5;

      end;

      A() c= ( dom R)

      proof

        let x be object;

        assume x in A();

        then

        reconsider x9 = x as Element of A();

        P[x9, x9] by A1;

        then [x, x] in R by A5;

        hence thesis by XTUPLE_0:def 12;

      end;

      then ( dom R) = A();

      then

       A13: A() c= ( field R) by XBOOLE_1: 7;

      ( field R) = (( dom R) \/ ( rng R));

      then

       A14: ( field R) = A() by A13;

      

       A15: R is_reflexive_in A() by A1, A5;

      

       A16: A() has_upper_Zorn_property_wrt R

      proof

        let Y such that

         A17: Y c= A() and

         A18: (R |_2 Y) is being_linear-order;

        for x,y be Element of A() st x in Y & y in Y holds P[x, y] or P[y, x]

        proof

          let x,y be Element of A() such that

           A19: x in Y and

           A20: y in Y;

          

           A21: (R |_2 Y) is reflexive connected by A18;

          Y c= ( field (R |_2 Y))

          proof

            let x be object;

            assume

             A22: x in Y;

            then

             A23: [x, x] in [:Y, Y:] by ZFMISC_1: 87;

             [x, x] in R by A15, A17, A22;

            then [x, x] in (R |_2 Y) by A23, XBOOLE_0:def 4;

            hence thesis by RELAT_1: 15;

          end;

          

          then

           A24: Y = ( field ((R |_2 Y) |_2 Y)) by A21, Lm7

          .= ( field (R |_2 Y)) by WELLORD1: 21;

          then

           A25: (R |_2 Y) is_connected_in Y by A21;

          

           A26: (R |_2 Y) is_reflexive_in Y by A21, A24;

          x = y or x <> y;

          then [x, y] in (R |_2 Y) or [y, x] in (R |_2 Y) by A19, A20, A25, A26;

          then [x, y] in R or [y, x] in R by XBOOLE_0:def 4;

          hence thesis by A5;

        end;

        then

        consider y be Element of A() such that

         A27: for x be Element of A() st x in Y holds P[x, y] by A4, A17;

        take y;

        thus y in A();

        let x;

        assume

         A28: x in Y;

        then P[x, y] by A17, A27;

        hence thesis by A5, A17, A28;

      end;

      R is_antisymmetric_in A()

      proof

        let x,y be object;

        assume that

         A29: x in A() and

         A30: y in A();

        reconsider x9 = x, y9 = y as Element of A() by A29, A30;

        assume that

         A31: [x, y] in R and

         A32: [y, x] in R;

        

         A33: P[y9, x9] by A5, A32;

        P[x9, y9] by A5, A31;

        hence thesis by A2, A33;

      end;

      then R partially_orders A() by A15, A6;

      then

      consider x such that

       A34: x is_maximal_in R by A14, A16, Th63;

      take x;

      thus x is Element of A() by A14, A34;

      let y be Element of A();

      assume x <> y;

      then

       A35: not [x, y] in R by A14, A34;

      x in A() by A14, A34;

      hence thesis by A5, A35;

    end;

    scheme :: ORDERS_1:sch2

    ZornMin { A() -> non empty set , P[ set, set] } :

ex x be Element of A() st for y be Element of A() st x <> y holds not P[y, x]

      provided

       A1: for x be Element of A() holds P[x, x]

       and

       A2: for x,y be Element of A() st P[x, y] & P[y, x] holds x = y

       and

       A3: for x,y,z be Element of A() st P[x, y] & P[y, z] holds P[x, z]

       and

       A4: for X st X c= A() & (for x,y be Element of A() st x in X & y in X holds P[x, y] or P[y, x]) holds ex y be Element of A() st for x be Element of A() st x in X holds P[y, x];

      consider R be Relation of A() such that

       A5: for x,y be Element of A() holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

      

       A6: R is_transitive_in A()

      proof

        let x,y,z be object;

        assume that

         A7: x in A() and

         A8: y in A() and

         A9: z in A();

        reconsider x9 = x, y9 = y, z9 = z as Element of A() by A7, A8, A9;

        assume that

         A10: [x, y] in R and

         A11: [y, z] in R;

        

         A12: P[y9, z9] by A5, A11;

        P[x9, y9] by A5, A10;

        then P[x9, z9] by A3, A12;

        hence thesis by A5;

      end;

      A() c= ( dom R)

      proof

        let x be object;

        assume x in A();

        then

        reconsider x9 = x as Element of A();

        P[x9, x9] by A1;

        then [x, x] in R by A5;

        hence thesis by XTUPLE_0:def 12;

      end;

      then ( dom R) = A();

      then

       A13: A() c= ( field R) by XBOOLE_1: 7;

      ( field R) = (( dom R) \/ ( rng R));

      then

       A14: ( field R) = A() by A13;

      

       A15: R is_reflexive_in A() by A1, A5;

      

       A16: A() has_lower_Zorn_property_wrt R

      proof

        let Y such that

         A17: Y c= A() and

         A18: (R |_2 Y) is being_linear-order;

        for x,y be Element of A() st x in Y & y in Y holds P[x, y] or P[y, x]

        proof

          let x,y be Element of A() such that

           A19: x in Y and

           A20: y in Y;

          

           A21: (R |_2 Y) is reflexive connected by A18;

          Y c= ( field (R |_2 Y))

          proof

            let x be object;

            assume

             A22: x in Y;

            then

             A23: [x, x] in [:Y, Y:] by ZFMISC_1: 87;

             [x, x] in R by A15, A17, A22;

            then [x, x] in (R |_2 Y) by A23, XBOOLE_0:def 4;

            hence thesis by RELAT_1: 15;

          end;

          

          then

           A24: Y = ( field ((R |_2 Y) |_2 Y)) by A21, Lm7

          .= ( field (R |_2 Y)) by WELLORD1: 21;

          then

           A25: (R |_2 Y) is_connected_in Y by A21;

          

           A26: (R |_2 Y) is_reflexive_in Y by A21, A24;

          x = y or x <> y;

          then [x, y] in (R |_2 Y) or [y, x] in (R |_2 Y) by A19, A20, A25, A26;

          then [x, y] in R or [y, x] in R by XBOOLE_0:def 4;

          hence thesis by A5;

        end;

        then

        consider y be Element of A() such that

         A27: for x be Element of A() st x in Y holds P[y, x] by A4, A17;

        take y;

        thus y in A();

        let x;

        assume

         A28: x in Y;

        then P[y, x] by A17, A27;

        hence thesis by A5, A17, A28;

      end;

      R is_antisymmetric_in A()

      proof

        let x,y be object;

        assume that

         A29: x in A() and

         A30: y in A();

        reconsider x9 = x, y9 = y as Element of A() by A29, A30;

        assume that

         A31: [x, y] in R and

         A32: [y, x] in R;

        

         A33: P[y9, x9] by A5, A32;

        P[x9, y9] by A5, A31;

        hence thesis by A2, A33;

      end;

      then R partially_orders A() by A15, A6;

      then

      consider x such that

       A34: x is_minimal_in R by A14, A16, Th64;

      take x;

      thus x is Element of A() by A14, A34;

      let y be Element of A();

      assume x <> y;

      then

       A35: not [y, x] in R by A14, A34;

      x in A() by A14, A34;

      hence thesis by A5, A35;

    end;

    theorem :: ORDERS_1:69

    R partially_orders X & ( field R) = X implies ex P st R c= P & P linearly_orders X & ( field P) = X

    proof

      assume that

       A1: R partially_orders X and

       A2: ( field R) = X;

      defpred P[ object] means ex P st $1 = P & R c= P & P partially_orders X & ( field P) = X;

      consider Rel be set such that

       A3: for x be object holds x in Rel iff x in ( bool [:X, X:]) & P[x] from XBOOLE_0:sch 1;

      

       A4: for Z st Z <> {} & Z c= Rel & Z is c=-linear holds ( union Z) in Rel

      proof

        reconsider T = [:X, X:] as Relation;

        let Z;

        assume that

         A5: Z <> {} and

         A6: Z c= Rel and

         A7: Z is c=-linear;

        

         A8: ( union ( bool [:X, X:])) = T by ZFMISC_1: 81;

        Z c= ( bool [:X, X:]) by A3, A6;

        then

         A9: ( union Z) c= ( union ( bool [:X, X:])) by ZFMISC_1: 77;

        then

        reconsider S = ( union Z) as Relation;

        set y = the Element of Z;

        y in Rel by A5, A6;

        then

        consider P such that

         A10: y = P and

         A11: R c= P and

         A12: P partially_orders X and ( field P) = X by A3;

        

         A13: S is_antisymmetric_in X

        proof

          let x,y be object;

          assume that

           A14: x in X and

           A15: y in X and

           A16: [x, y] in S and

           A17: [y, x] in S;

          consider X1 such that

           A18: [x, y] in X1 and

           A19: X1 in Z by A16, TARSKI:def 4;

          consider P1 be Relation such that

           A20: X1 = P1 and R c= P1 and

           A21: P1 partially_orders X and ( field P1) = X by A3, A6, A19;

          consider X2 such that

           A22: [y, x] in X2 and

           A23: X2 in Z by A17, TARSKI:def 4;

          (X1,X2) are_c=-comparable by A7, A19, A23;

          then

           A24: X1 c= X2 or X2 c= X1;

          consider P2 be Relation such that

           A25: X2 = P2 and R c= P2 and

           A26: P2 partially_orders X and ( field P2) = X by A3, A6, A23;

          

           A27: P2 is_antisymmetric_in X by A26;

          P1 is_antisymmetric_in X by A21;

          hence thesis by A14, A15, A18, A22, A24, A20, A25, A27;

        end;

        

         A28: S is_transitive_in X

        proof

          let x,y,z be object;

          assume that

           A29: x in X and

           A30: y in X and

           A31: z in X and

           A32: [x, y] in S and

           A33: [y, z] in S;

          consider X1 such that

           A34: [x, y] in X1 and

           A35: X1 in Z by A32, TARSKI:def 4;

          consider P1 be Relation such that

           A36: X1 = P1 and R c= P1 and

           A37: P1 partially_orders X and ( field P1) = X by A3, A6, A35;

          consider X2 such that

           A38: [y, z] in X2 and

           A39: X2 in Z by A33, TARSKI:def 4;

          (X1,X2) are_c=-comparable by A7, A35, A39;

          then

           A40: X1 c= X2 or X2 c= X1;

          consider P2 be Relation such that

           A41: X2 = P2 and R c= P2 and

           A42: P2 partially_orders X and ( field P2) = X by A3, A6, A39;

          

           A43: P2 is_transitive_in X by A42;

          P1 is_transitive_in X by A37;

          then [x, z] in P1 or [x, z] in P2 by A29, A30, A31, A34, A38, A40, A36, A41, A43;

          hence thesis by A35, A39, A36, A41, TARSKI:def 4;

        end;

        

         A44: P is_reflexive_in X by A12;

        S is_reflexive_in X

        proof

          let x be object;

          assume x in X;

          then [x, x] in P by A44;

          hence thesis by A5, A10, TARSKI:def 4;

        end;

        then

         A45: S partially_orders X by A28, A13;

        

         A46: ( field S) c= X

        proof

          let x be object;

           A47:

          now

            assume x in ( dom S);

            then

            consider y be object such that

             A48: [x, y] in S by XTUPLE_0:def 12;

            consider Y such that

             A49: [x, y] in Y and

             A50: Y in Z by A48, TARSKI:def 4;

            ex P st Y = P & R c= P & P partially_orders X & ( field P) = X by A3, A6, A50;

            hence thesis by A49, RELAT_1: 15;

          end;

           A51:

          now

            assume x in ( rng S);

            then

            consider y be object such that

             A52: [y, x] in S by XTUPLE_0:def 13;

            consider Y such that

             A53: [y, x] in Y and

             A54: Y in Z by A52, TARSKI:def 4;

            ex P st Y = P & R c= P & P partially_orders X & ( field P) = X by A3, A6, A54;

            hence thesis by A53, RELAT_1: 15;

          end;

          assume x in ( field S);

          hence thesis by A47, A51, XBOOLE_0:def 3;

        end;

        

         A55: R c= S by A5, A10, A11, TARSKI:def 4;

        then X c= ( field S) by A2, RELAT_1: 16;

        then ( field S) = X by A46;

        hence thesis by A3, A9, A8, A55, A45;

      end;

      R c= [:X, X:] by A2, Lm6;

      then Rel <> {} by A1, A2, A3;

      then

      consider Y such that

       A56: Y in Rel and

       A57: for Z st Z in Rel & Z <> Y holds not Y c= Z by A4, Th67;

      consider P such that

       A58: Y = P and

       A59: R c= P and

       A60: P partially_orders X and

       A61: ( field P) = X by A3, A56;

      take P;

      thus R c= P by A59;

      thus

       A62: P is_reflexive_in X & P is_transitive_in X & P is_antisymmetric_in X by A60;

      thus P is_connected_in X

      proof

        let x,y be object such that

         A63: x in X and

         A64: y in X and x <> y and

         A65: not [x, y] in P and

         A66: not [y, x] in P;

        defpred Q[ object, object] means [$1, $2] in P or [$1, x] in P & [y, $2] in P;

        consider Q be Relation such that

         A67: for z,u be object holds [z, u] in Q iff z in X & u in X & Q[z, u] from RELAT_1:sch 1;

        

         A68: ( field Q) c= X

        proof

          let z be object;

           A69:

          now

            assume z in ( dom Q);

            then ex u be object st [z, u] in Q by XTUPLE_0:def 12;

            hence thesis by A67;

          end;

           A70:

          now

            assume z in ( rng Q);

            then ex u be object st [u, z] in Q by XTUPLE_0:def 13;

            hence thesis by A67;

          end;

          assume z in ( field Q);

          hence thesis by A69, A70, XBOOLE_0:def 3;

        end;

        

         A71: P c= Q

        proof

          let z,u be object;

          assume

           A72: [z, u] in P;

          then

           A73: u in ( field P) by RELAT_1: 15;

          z in ( field P) by A72, RELAT_1: 15;

          hence thesis by A61, A67, A72, A73;

        end;

        then X c= ( field Q) by A61, RELAT_1: 16;

        then

         A74: ( field Q) = X by A68;

        

         A75: Q is_transitive_in X

        proof

          let a,b,c be object;

          assume that

           A76: a in X and

           A77: b in X and

           A78: c in X and

           A79: [a, b] in Q and

           A80: [b, c] in Q;

          

           A81: [b, c] in P or [b, x] in P & [y, c] in P by A67, A80;

           [a, b] in P or [a, x] in P & [y, b] in P by A67, A79;

          then [a, c] in P or [a, x] in P & [y, c] in P or [a, x] in P & [y, c] in P or [y, x] in P by A62, A63, A64, A76, A77, A78, A81;

          hence thesis by A66, A67, A76, A78;

        end;

        

         A82: Q is_antisymmetric_in X

        proof

          let a,b be object;

          assume that

           A83: a in X and

           A84: b in X and

           A85: [a, b] in Q and

           A86: [b, a] in Q;

          

           A87: [b, a] in P or [b, x] in P & [y, a] in P by A67, A86;

           [a, b] in P or [a, x] in P & [y, b] in P by A67, A85;

          then a = b or [a, x] in P & [y, a] in P or [y, x] in P by A62, A63, A64, A83, A84, A87;

          hence thesis by A62, A63, A64, A66, A83;

        end;

        Q is_reflexive_in X by A62, A67;

        then

         A88: Q partially_orders X by A75, A82;

        

         A89: Q c= [:X, X:]

        proof

          let y,z be object;

          assume

           A90: [y, z] in Q;

          then

           A91: z in X by A67;

          y in X by A67, A90;

          hence thesis by A91, ZFMISC_1: 87;

        end;

        R c= Q by A59, A71;

        then Q in Rel by A3, A89, A74, A88;

        then

         A92: Q = P by A57, A58, A71;

        

         A93: [y, y] in P by A62, A64;

         [x, x] in P by A62, A63;

        hence contradiction by A63, A64, A65, A67, A92, A93;

      end;

      thus thesis by A61;

    end;

    theorem :: ORDERS_1:70

    R c= [:( field R), ( field R):] by Lm6;

    theorem :: ORDERS_1:71

    R is reflexive & X c= ( field R) implies ( field (R |_2 X)) = X by Lm7;

    theorem :: ORDERS_1:72

    R is_reflexive_in X implies (R |_2 X) is reflexive by Lm8;

    theorem :: ORDERS_1:73

    R is_transitive_in X implies (R |_2 X) is transitive by Lm9;

    theorem :: ORDERS_1:74

    R is_antisymmetric_in X implies (R |_2 X) is antisymmetric by Lm10;

    theorem :: ORDERS_1:75

    R is_connected_in X implies (R |_2 X) is connected by Lm11;

    theorem :: ORDERS_1:76

    R is_connected_in X & Y c= X implies R is_connected_in Y;

    theorem :: ORDERS_1:77

    R well_orders X & Y c= X implies R well_orders Y by Lm18;

    theorem :: ORDERS_1:78

    R is connected implies (R ~ ) is connected by Lm5;

    theorem :: ORDERS_1:79

    R is_reflexive_in X implies (R ~ ) is_reflexive_in X by Lm12;

    theorem :: ORDERS_1:80

    R is_transitive_in X implies (R ~ ) is_transitive_in X by Lm13;

    theorem :: ORDERS_1:81

    R is_antisymmetric_in X implies (R ~ ) is_antisymmetric_in X by Lm14;

    theorem :: ORDERS_1:82

    R is_connected_in X implies (R ~ ) is_connected_in X by Lm15;

    theorem :: ORDERS_1:83

    ((R |_2 X) ~ ) = ((R ~ ) |_2 X) by Lm16;

    theorem :: ORDERS_1:84

    (R |_2 {} ) = {} by Lm17;

    begin

    theorem :: ORDERS_1:85

    Z is finite & Z c= ( rng f) implies ex Y st Y c= ( dom f) & Y is finite & (f .: Y) = Z

    proof

      assume that

       A1: Z is finite and

       A2: Z c= ( rng f);

      per cases ;

        suppose

         A3: Z = {} ;

        take Y = {} ;

        thus Y c= ( dom f) & Y is finite;

        thus thesis by A3;

      end;

        suppose

         A4: Z <> {} ;

        deffunc F( object) = (f " {$1});

        consider g be Function such that

         A5: ( dom g) = Z and

         A6: for x be object st x in Z holds (g . x) = F(x) from FUNCT_1:sch 3;

        reconsider AA = ( rng g) as non empty set by A4, A5, RELAT_1: 42;

        set ff = the Choice_Function of AA;

        take Y = (ff .: AA);

        

         A7: for X be set st X in AA holds X <> {}

        proof

          let X be set;

          assume X in AA;

          then

          consider x be object such that

           A8: x in ( dom g) and

           A9: (g . x) = X by FUNCT_1:def 3;

          (g . x) = (f " {x}) by A5, A6, A8;

          hence thesis by A2, A5, A8, A9, FUNCT_1: 72;

        end;

        then

         A10: not {} in AA;

        thus

         A11: Y c= ( dom f)

        proof

          let x be object;

          assume x in Y;

          then

          consider y be object such that y in ( dom ff) and

           A12: y in AA and

           A13: (ff . y) = x by FUNCT_1:def 6;

          y in (g .: Z) by A5, A12, RELAT_1: 113;

          then

          consider z be object such that z in ( dom g) and

           A14: z in Z and

           A15: (g . z) = y by FUNCT_1:def 6;

          

           A16: (g . z) = (f " {z}) by A6, A14;

          x in (g . z) by A10, A12, A13, A15, Lm2;

          hence thesis by A16, FUNCT_1:def 7;

        end;

        AA = (g .: Z) by A5, RELAT_1: 113;

        hence Y is finite by A1;

        set z = the Element of AA;

        set y = the Element of z;

        z <> {} by A7;

        then y in z;

        then

        reconsider AA9 = ( union AA) as non empty set by TARSKI:def 4;

        reconsider f9 = ff as Function of AA, AA9 by A10, Lm3;

        

         A17: ( dom f9) = AA by FUNCT_2:def 1;

        for x be object holds x in (f .: Y) iff x in Z

        proof

          let x be object;

          thus x in (f .: Y) implies x in Z

          proof

            assume x in (f .: Y);

            then

            consider y be object such that y in ( dom f) and

             A18: y in Y and

             A19: (f . y) = x by FUNCT_1:def 6;

            consider z be object such that

             A20: z in ( dom ff) and z in AA and

             A21: (ff . z) = y by A18, FUNCT_1:def 6;

            consider a be object such that

             A22: a in ( dom g) and

             A23: (g . a) = z by A20, FUNCT_1:def 3;

            (g . a) = (f " {a}) by A5, A6, A22;

            then y in (f " {a}) by A10, A20, A21, A23, Lm2;

            then (f . y) in {a} by FUNCT_1:def 7;

            hence thesis by A5, A19, A22, TARSKI:def 1;

          end;

          set y = (ff . (g . x));

          assume

           A24: x in Z;

          then

           A25: (g . x) in AA by A5, FUNCT_1:def 3;

          (g . x) = (f " {x}) by A6, A24;

          then y in (f " {x}) by A10, A25, Lm2;

          then (f . y) in {x} by FUNCT_1:def 7;

          then

           A26: (f . y) = x by TARSKI:def 1;

          (ff . (g . x)) in ( rng ff) by A17, A25, FUNCT_1:def 3;

          then y in Y by A17, RELAT_1: 113;

          hence thesis by A11, A26, FUNCT_1:def 6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end;

    theorem :: ORDERS_1:86

    

     Th86: ( field R) is finite implies R is finite

    proof

      assume ( field R) is finite;

      then

      reconsider A = ( field R) as finite set;

      R c= [:A, A:] by Lm6;

      hence thesis;

    end;

    theorem :: ORDERS_1:87

    ( dom R) is finite & ( rng R) is finite implies R is finite

    proof

      assume that

       A1: ( dom R) is finite and

       A2: ( rng R) is finite;

      ( field R) is finite by A1, A2;

      hence thesis by Th86;

    end;

    registration

      cluster ( order_type_of {} ) -> empty;

      coherence

      proof

        ( {} ,( RelIncl {} )) are_isomorphic by WELLORD1: 38;

        hence thesis by WELLORD2:def 2;

      end;

    end

    theorem :: ORDERS_1:88

    for O be Ordinal holds ( order_type_of ( RelIncl O)) = O

    proof

      let O be Ordinal;

      ( RelIncl O) is well-ordering & (( RelIncl O),( RelIncl O)) are_isomorphic by WELLORD1: 38;

      hence thesis by WELLORD2:def 2;

    end;

    definition

      let X be set;

      :: original: RelIncl

      redefine

      func RelIncl X -> Order of X ;

      coherence

      proof

        now

          let x be object;

          assume

           A1: x in ( RelIncl X);

          then

          consider y,z be object such that

           A2: x = [y, z] by RELAT_1:def 1;

          z in ( field ( RelIncl X)) by A1, A2, RELAT_1: 15;

          then

           A3: z in X by WELLORD2:def 1;

          y in ( field ( RelIncl X)) by A1, A2, RELAT_1: 15;

          then y in X by WELLORD2:def 1;

          hence x in [:X, X:] by A2, A3, ZFMISC_1: 87;

        end;

        then

        reconsider R = ( RelIncl X) as Relation of X by TARSKI:def 3;

        ( field R) = X & R is reflexive by WELLORD2:def 1;

        then R is_reflexive_in X;

        then ( dom R) = X by Th13;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    theorem :: ORDERS_1:89

     not {} in M implies for Ch be Choice_Function of M holds for X st X in M holds (Ch . X) in X by Lm2;

    theorem :: ORDERS_1:90

     not {} in M implies for Ch be Choice_Function of M holds Ch is Function of M, ( union M) by Lm3;