wellord1.miz



    begin

    reserve a,b,c,d,x,y,z for object,

X,Y,Z for set;

    reserve R,S,T for Relation;

    

     Lm1: R is reflexive iff for x st x in ( field R) holds [x, x] in R by RELAT_2:def 1, RELAT_2:def 9;

    

     Lm2: R is transitive iff for x, y, z st [x, y] in R & [y, z] in R holds [x, z] in R

    proof

      thus R is transitive implies for x, y, z st [x, y] in R & [y, z] in R holds [x, z] in R

      proof

        assume R is transitive;

        then

         A1: R is_transitive_in ( field R) by RELAT_2:def 16;

        let x, y, z;

        assume that

         A2: [x, y] in R and

         A3: [y, z] in R;

        

         A4: z in ( field R) by A3, RELAT_1: 15;

        x in ( field R) & y in ( field R) by A2, RELAT_1: 15;

        hence thesis by A1, A2, A3, A4, RELAT_2:def 8;

      end;

      assume for x, y, z st [x, y] in R & [y, z] in R holds [x, z] in R;

      then for x, y, z st x in ( field R) & y in ( field R) & z in ( field R) & [x, y] in R & [y, z] in R holds [x, z] in R;

      then R is_transitive_in ( field R) by RELAT_2:def 8;

      hence thesis by RELAT_2:def 16;

    end;

    

     Lm3: R is antisymmetric iff for x, y st [x, y] in R & [y, x] in R holds x = y

    proof

      thus R is antisymmetric implies for x, y st [x, y] in R & [y, x] in R holds x = y

      proof

        assume R is antisymmetric;

        then

         A1: R is_antisymmetric_in ( field R) by RELAT_2:def 12;

        let x, y;

        assume that

         A2: [x, y] in R and

         A3: [y, x] in R;

        x in ( field R) & y in ( field R) by A2, RELAT_1: 15;

        hence thesis by A1, A2, A3, RELAT_2:def 4;

      end;

      assume for x, y st [x, y] in R & [y, x] in R holds x = y;

      then for x, y st x in ( field R) & y in ( field R) & [x, y] in R & [y, x] in R holds x = y;

      then R is_antisymmetric_in ( field R) by RELAT_2:def 4;

      hence thesis by RELAT_2:def 12;

    end;

    

     Lm4: R is connected iff for x, y st x in ( field R) & y in ( field R) & x <> y holds [x, y] in R or [y, x] in R by RELAT_2:def 6, RELAT_2:def 14;

    definition

      let R;

      let a be object;

      :: WELLORD1:def1

      func R -Seg (a) -> set equals (( Coim (R,a)) \ {a});

      coherence ;

    end

    theorem :: WELLORD1:1

    

     Th1: x in (R -Seg a) iff x <> a & [x, a] in R

    proof

      hereby

        assume

         A1: x in (R -Seg a);

        hence x <> a by ZFMISC_1: 56;

        ex y be object st [x, y] in R & y in {a} by A1, RELAT_1:def 14;

        hence [x, a] in R by TARSKI:def 1;

      end;

      assume that

       A2: x <> a and

       A3: [x, a] in R;

      a in {a} by TARSKI:def 1;

      then x in ( Coim (R,a)) by A3, RELAT_1:def 14;

      hence thesis by A2, ZFMISC_1: 56;

    end;

    theorem :: WELLORD1:2

    

     Th2: x in ( field R) or (R -Seg x) = {}

    proof

      assume

       A1: not x in ( field R);

      set y = the Element of (R -Seg x);

      assume (R -Seg x) <> {} ;

      then [y, x] in R by Th1;

      hence contradiction by A1, RELAT_1: 15;

    end;

    definition

      let R;

      :: WELLORD1:def2

      attr R is well_founded means

      : Def2: for Y st Y c= ( field R) & Y <> {} holds ex a st a in Y & (R -Seg a) misses Y;

      let X;

      :: WELLORD1:def3

      pred R is_well_founded_in X means for Y st Y c= X & Y <> {} holds ex a st a in Y & (R -Seg a) misses Y;

    end

    theorem :: WELLORD1:3

    R is well_founded iff R is_well_founded_in ( field R);

    definition

      let R;

      :: WELLORD1:def4

      attr R is well-ordering means R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded;

      let X;

      :: WELLORD1:def5

      pred R well_orders X means R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X;

    end

    registration

      cluster well-ordering -> reflexive transitive antisymmetric connected well_founded for Relation;

      coherence ;

      cluster reflexive transitive antisymmetric connected well_founded -> well-ordering for Relation;

      coherence ;

    end

    theorem :: WELLORD1:4

    R well_orders ( field R) iff R is well-ordering

    proof

      thus R well_orders ( field R) implies R is well-ordering

      proof

        assume R is_reflexive_in ( field R) & R is_transitive_in ( field R) & R is_antisymmetric_in ( field R) & R is_connected_in ( field R) & R is_well_founded_in ( field R);

        hence R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16;

      end;

      assume R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded;

      hence R is_reflexive_in ( field R) & R is_transitive_in ( field R) & R is_antisymmetric_in ( field R) & R is_connected_in ( field R) & R is_well_founded_in ( field R) by RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 14, RELAT_2:def 16;

    end;

    theorem :: WELLORD1:5

    R well_orders X implies for Y st Y c= X & Y <> {} holds ex a st a in Y & for b st b in Y holds [a, b] in R

    proof

      assume

       A1: R well_orders X;

      then

       A2: R is_reflexive_in X;

      

       A3: R is_connected_in X by A1;

      let Y;

      assume that

       A4: Y c= X and

       A5: Y <> {} ;

      R is_well_founded_in X by A1;

      then

      consider a such that

       A6: a in Y and

       A7: (R -Seg a) misses Y by A4, A5;

      take a;

      thus a in Y by A6;

      let b;

      assume

       A8: b in Y;

      then not b in (R -Seg a) by A7, XBOOLE_0: 3;

      then a = b or not [b, a] in R by Th1;

      then a <> b implies [a, b] in R by A3, A4, A6, A8, RELAT_2:def 6;

      hence thesis by A2, A4, A6, RELAT_2:def 1;

    end;

    theorem :: WELLORD1:6

    

     Th6: R is well-ordering implies for Y st Y c= ( field R) & Y <> {} holds ex a st a in Y & for b st b in Y holds [a, b] in R

    proof

      assume

       A1: R is well-ordering;

      let Y;

      assume that

       A2: Y c= ( field R) and

       A3: Y <> {} ;

      consider a such that

       A4: a in Y and

       A5: (R -Seg a) misses Y by A1, A2, A3, Def2;

      take a;

      thus a in Y by A4;

      let b;

      assume

       A6: b in Y;

      then not b in (R -Seg a) by A5, XBOOLE_0: 3;

      then a = b or not [b, a] in R by Th1;

      then a <> b implies [a, b] in R by A1, A2, A4, A6, Lm4;

      hence thesis by A1, A2, A4, Lm1;

    end;

    theorem :: WELLORD1:7

    for R st R is well-ordering & ( field R) <> {} holds ex a st a in ( field R) & for b st b in ( field R) holds [a, b] in R by Th6;

    theorem :: WELLORD1:8

    for R st R is well-ordering holds for a st a in ( field R) holds (for b st b in ( field R) holds [b, a] in R) or ex b st b in ( field R) & [a, b] in R & for c st c in ( field R) & [a, c] in R holds c = a or [b, c] in R

    proof

      let R;

      assume

       A1: R is well-ordering;

      let a such that

       A2: a in ( field R);

      defpred P[ object] means not [$1, a] in R;

      given b such that

       A3: b in ( field R) & not [b, a] in R;

      consider Z such that

       A4: for c be object holds c in Z iff c in ( field R) & P[c] from XBOOLE_0:sch 1;

      for b be object holds b in Z implies b in ( field R) by A4;

      then

       A5: Z c= ( field R);

      Z <> {} by A3, A4;

      then

      consider d such that

       A6: d in Z and

       A7: for c st c in Z holds [d, c] in R by A1, A5, Th6;

      take d;

      thus

       A8: d in ( field R) by A4, A6;

      

       A9: not [d, a] in R by A4, A6;

      then a <> d by A6, A7;

      hence [a, d] in R by A1, A2, A8, A9, Lm4;

      let c;

      assume that

       A10: c in ( field R) and

       A11: [a, c] in R;

      assume c <> a;

      then not [c, a] in R by A1, A11, Lm3;

      then c in Z by A4, A10;

      hence thesis by A7;

    end;

    reserve F,G for Function;

    theorem :: WELLORD1:9

    

     Th9: (R -Seg a) c= ( field R)

    proof

      let b be object;

      assume b in (R -Seg a);

      then [b, a] in R by Th1;

      hence thesis by RELAT_1: 15;

    end;

    definition

      let R, Y;

      :: WELLORD1:def6

      func R |_2 Y -> Relation equals (R /\ [:Y, Y:]);

      coherence ;

    end

    theorem :: WELLORD1:10

    

     Th10: (R |_2 X) = ((X |` R) | X)

    proof

      let x,y be object;

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

      proof

        assume

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

        then

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

        then

         A3: x in X by ZFMISC_1: 87;

        

         A4: y in X by A2, ZFMISC_1: 87;

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

        then [x, y] in (X |` R) by A4, RELAT_1:def 12;

        hence thesis by A3, RELAT_1:def 11;

      end;

      assume

       A5: [x, y] in ((X |` R) | X);

      then

       A6: [x, y] in (X |` R) by RELAT_1:def 11;

      then

       A7: [x, y] in R by RELAT_1:def 12;

      

       A8: y in X by A6, RELAT_1:def 12;

      x in X by A5, RELAT_1:def 11;

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

      hence thesis by A7, XBOOLE_0:def 4;

    end;

    theorem :: WELLORD1:11

    

     Th11: (R |_2 X) = (X |` (R | X))

    proof

      

      thus (R |_2 X) = ((X |` R) | X) by Th10

      .= (X |` (R | X)) by RELAT_1: 109;

    end;

    

     Lm5: ( dom (X |` R)) c= ( dom R)

    proof

      let x be object;

      assume x in ( dom (X |` R));

      then

      consider y be object such that

       A1: [x, y] in (X |` R) by XTUPLE_0:def 12;

       [x, y] in R by A1, RELAT_1:def 12;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: WELLORD1:12

    

     Th12: x in ( field (R |_2 X)) implies x in ( field R) & x in X

    proof

      

       A1: ( dom ((X |` R) | X)) = (( dom (X |` R)) /\ X) & ( rng (X |` (R | X))) = (( rng (R | X)) /\ X) by RELAT_1: 61, RELAT_1: 88;

      assume x in ( field (R |_2 X));

      then

       A2: x in ( dom (R |_2 X)) or x in ( rng (R |_2 X)) by XBOOLE_0:def 3;

      

       A3: ( dom (X |` R)) c= ( dom R) & ( rng (R | X)) c= ( rng R) by Lm5, RELAT_1: 70;

      (R |_2 X) = ((X |` R) | X) & (R |_2 X) = (X |` (R | X)) by Th10, Th11;

      then x in ( dom (X |` R)) & x in X or x in ( rng (R | X)) & x in X by A2, A1, XBOOLE_0:def 4;

      hence thesis by A3, XBOOLE_0:def 3;

    end;

    theorem :: WELLORD1:13

    

     Th13: ( field (R |_2 X)) c= ( field R) & ( field (R |_2 X)) c= X by Th12;

    theorem :: WELLORD1:14

    

     Th14: ((R |_2 X) -Seg a) c= (R -Seg a)

    proof

      let x be object;

      assume

       A1: x in ((R |_2 X) -Seg a);

      then [x, a] in (R |_2 X) by Th1;

      then

       A2: [x, a] in R by XBOOLE_0:def 4;

      x <> a by A1, Th1;

      hence thesis by A2, Th1;

    end;

    theorem :: WELLORD1:15

    

     Th15: R is reflexive implies (R |_2 X) is reflexive

    proof

      assume

       A1: R is reflexive;

      now

        let a;

        assume

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

        then a in X by Th12;

        then

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

        a in ( field R) by A2, Th12;

        then [a, a] in R by A1, Lm1;

        hence [a, a] in (R |_2 X) by A3, XBOOLE_0:def 4;

      end;

      hence thesis by Lm1;

    end;

    theorem :: WELLORD1:16

    

     Th16: R is connected implies (R |_2 Y) is connected

    proof

      assume

       A1: R is connected;

      now

        let a, b;

        assume that

         A2: a in ( field (R |_2 Y)) & b in ( field (R |_2 Y)) and

         A3: a <> b;

        a in Y & b in Y by A2, Th12;

        then

         A4: [a, b] in [:Y, Y:] & [b, a] in [:Y, Y:] by ZFMISC_1: 87;

        a in ( field R) & b in ( field R) by A2, Th12;

        then [a, b] in R or [b, a] in R by A1, A3, Lm4;

        hence [a, b] in (R |_2 Y) or [b, a] in (R |_2 Y) by A4, XBOOLE_0:def 4;

      end;

      hence thesis by Lm4;

    end;

    theorem :: WELLORD1:17

    

     Th17: R is transitive implies (R |_2 Y) is transitive

    proof

      assume

       A1: R is transitive;

      now

        let a, b, c;

        assume that

         A2: [a, b] in (R |_2 Y) and

         A3: [b, c] in (R |_2 Y);

         [a, b] in R & [b, c] in R by A2, A3, XBOOLE_0:def 4;

        then

         A4: [a, c] in R by A1, Lm2;

         [b, c] in [:Y, Y:] by A3, XBOOLE_0:def 4;

        then

         A5: c in Y by ZFMISC_1: 87;

         [a, b] in [:Y, Y:] by A2, XBOOLE_0:def 4;

        then a in Y by ZFMISC_1: 87;

        then [a, c] in [:Y, Y:] by A5, ZFMISC_1: 87;

        hence [a, c] in (R |_2 Y) by A4, XBOOLE_0:def 4;

      end;

      hence thesis by Lm2;

    end;

    theorem :: WELLORD1:18

    

     Th18: R is antisymmetric implies (R |_2 Y) is antisymmetric

    proof

      assume

       A1: R is antisymmetric;

      now

        let a, b;

        assume [a, b] in (R |_2 Y) & [b, a] in (R |_2 Y);

        then [a, b] in R & [b, a] in R by XBOOLE_0:def 4;

        hence a = b by A1, Lm3;

      end;

      hence thesis by Lm3;

    end;

    theorem :: WELLORD1:19

    

     Th19: ((R |_2 X) |_2 Y) = (R |_2 (X /\ Y))

    proof

      

      thus ((R |_2 X) |_2 Y) = (R /\ ( [:X, X:] /\ [:Y, Y:])) by XBOOLE_1: 16

      .= (R |_2 (X /\ Y)) by ZFMISC_1: 100;

    end;

    theorem :: WELLORD1:20

    ((R |_2 X) |_2 Y) = ((R |_2 Y) |_2 X)

    proof

      

      thus ((R |_2 X) |_2 Y) = (R |_2 (Y /\ X)) by Th19

      .= ((R |_2 Y) |_2 X) by Th19;

    end;

    theorem :: WELLORD1:21

    ((R |_2 Y) |_2 Y) = (R |_2 Y)

    proof

      let a,b be object;

      thus [a, b] in ((R |_2 Y) |_2 Y) implies [a, b] in (R |_2 Y) by XBOOLE_0:def 4;

      assume

       A1: [a, b] in (R |_2 Y);

      then [a, b] in [:Y, Y:] by XBOOLE_0:def 4;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: WELLORD1:22

    

     Th22: Z c= Y implies ((R |_2 Y) |_2 Z) = (R |_2 Z)

    proof

      assume

       A1: Z c= Y;

      let a,b be object;

      thus [a, b] in ((R |_2 Y) |_2 Z) implies [a, b] in (R |_2 Z)

      proof

        assume

         A2: [a, b] in ((R |_2 Y) |_2 Z);

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

        then

         A3: [a, b] in R by XBOOLE_0:def 4;

         [a, b] in [:Z, Z:] by A2, XBOOLE_0:def 4;

        hence thesis by A3, XBOOLE_0:def 4;

      end;

      assume

       A4: [a, b] in (R |_2 Z);

      then

       A5: [a, b] in R by XBOOLE_0:def 4;

      

       A6: [a, b] in [:Z, Z:] by A4, XBOOLE_0:def 4;

      then a in Z & b in Z by ZFMISC_1: 87;

      then [a, b] in [:Y, Y:] by A1, ZFMISC_1: 87;

      then [a, b] in (R |_2 Y) by A5, XBOOLE_0:def 4;

      hence thesis by A6, XBOOLE_0:def 4;

    end;

    theorem :: WELLORD1:23

    

     Th23: (R |_2 ( field R)) = R

    proof

      let x,y be object;

      thus [x, y] in (R |_2 ( field R)) implies [x, y] in R by XBOOLE_0:def 4;

      assume

       A1: [x, y] in R;

      then x in ( field R) & y in ( field R) by RELAT_1: 15;

      then [x, y] in [:( field R), ( field R):] by ZFMISC_1: 87;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: WELLORD1:24

    

     Th24: R is well_founded implies (R |_2 X) is well_founded

    proof

      assume

       A1: for Y st Y c= ( field R) & Y <> {} holds ex a st a in Y & (R -Seg a) misses Y;

      

       A2: ( field (R |_2 X)) c= ( field R) by Th13;

      let Y;

      assume Y c= ( field (R |_2 X)) & Y <> {} ;

      then

      consider a such that

       A3: a in Y and

       A4: (R -Seg a) misses Y by A1, A2, XBOOLE_1: 1;

      take a;

      thus a in Y by A3;

      assume not thesis;

      then

       A5: ex b be object st b in ((R |_2 X) -Seg a) & b in Y by XBOOLE_0: 3;

      ((R |_2 X) -Seg a) c= (R -Seg a) by Th14;

      hence contradiction by A4, A5, XBOOLE_0: 3;

    end;

    theorem :: WELLORD1:25

    

     Th25: R is well-ordering implies (R |_2 Y) is well-ordering by Th15, Th16, Th17, Th18, Th24;

    theorem :: WELLORD1:26

    

     Th26: R is well-ordering implies ((R -Seg a),(R -Seg b)) are_c=-comparable

    proof

      assume

       A1: R is well-ordering;

       A2:

      now

        assume

         A3: a in ( field R) & b in ( field R);

        now

          assume a <> b;

           A4:

          now

            assume

             A5: [b, a] in R;

            now

              let c be object;

              assume

               A6: c in (R -Seg b);

              then

               A7: [c, b] in R by Th1;

              then

               A8: [c, a] in R by A1, A5, Lm2;

              c <> b by A6, Th1;

              then c <> a by A1, A5, A7, Lm3;

              hence c in (R -Seg a) by A8, Th1;

            end;

            hence (R -Seg b) c= (R -Seg a);

          end;

          now

            assume

             A9: [a, b] in R;

            now

              let c be object;

              assume

               A10: c in (R -Seg a);

              then

               A11: [c, a] in R by Th1;

              then

               A12: [c, b] in R by A1, A9, Lm2;

              c <> a by A10, Th1;

              then c <> b by A1, A9, A11, Lm3;

              hence c in (R -Seg b) by A12, Th1;

            end;

            hence (R -Seg a) c= (R -Seg b);

          end;

          hence thesis by A1, A3, A4, Lm4;

        end;

        hence thesis;

      end;

      now

        assume (R -Seg a) = {} or (R -Seg b) = {} ;

        then (R -Seg a) c= (R -Seg b) or (R -Seg b) c= (R -Seg a);

        hence thesis;

      end;

      hence thesis by A2, Th2;

    end;

    theorem :: WELLORD1:27

    

     Th27: R is well-ordering & b in (R -Seg a) implies ((R |_2 (R -Seg a)) -Seg b) = (R -Seg b)

    proof

      assume that

       A1: R is well-ordering and

       A2: b in (R -Seg a);

      set S = (R |_2 (R -Seg a));

      now

        let c be object;

        assume

         A3: c in (R -Seg b);

        then

         A4: [c, b] in R by Th1;

        

         A5: [b, a] in R by A2, Th1;

        then

         A6: [c, a] in R by A1, A4, Lm2;

        

         A7: c <> b by A3, Th1;

        then c <> a by A1, A4, A5, Lm3;

        then c in (R -Seg a) by A6, Th1;

        then [c, b] in [:(R -Seg a), (R -Seg a):] by A2, ZFMISC_1: 87;

        then [c, b] in S by A4, XBOOLE_0:def 4;

        hence c in (S -Seg b) by A7, Th1;

      end;

      then

       A8: (R -Seg b) c= (S -Seg b);

      now

        let c be object;

        assume

         A9: c in (S -Seg b);

        then [c, b] in S by Th1;

        then

         A10: [c, b] in R by XBOOLE_0:def 4;

        c <> b by A9, Th1;

        hence c in (R -Seg b) by A10, Th1;

      end;

      then (S -Seg b) c= (R -Seg b);

      hence thesis by A8;

    end;

    theorem :: WELLORD1:28

    

     Th28: R is well-ordering & Y c= ( field R) implies (Y = ( field R) or (ex a st a in ( field R) & Y = (R -Seg a)) iff for a st a in Y holds for b st [b, a] in R holds b in Y)

    proof

      assume that

       A1: R is well-ordering and

       A2: Y c= ( field R);

      now

        given a such that a in ( field R) and

         A3: Y = (R -Seg a);

        let b such that

         A4: b in Y;

        

         A5: [b, a] in R by A3, A4, Th1;

        let c such that

         A6: [c, b] in R;

        

         A7: [c, a] in R by A1, A6, A5, Lm2;

        b <> a by A3, A4, Th1;

        then c <> a by A1, A6, A5, Lm3;

        hence c in Y by A3, A7, Th1;

      end;

      hence Y = ( field R) or (ex a st a in ( field R) & Y = (R -Seg a)) implies for a st a in Y holds for b st [b, a] in R holds b in Y by RELAT_1: 15;

      assume

       A8: for a st a in Y holds for b st [b, a] in R holds b in Y;

      assume Y <> ( field R);

      then ex d be object st not (d in ( field R) iff d in Y) by TARSKI: 2;

      then (( field R) \ Y) <> {} by A2, XBOOLE_0:def 5;

      then

      consider a such that

       A9: a in (( field R) \ Y) and

       A10: for b st b in (( field R) \ Y) holds [a, b] in R by A1, Th6;

       A11:

      now

        let b be object;

        assume

         A12: b in (R -Seg a);

        then

         A13: [b, a] in R by Th1;

        assume

         A14: not b in Y;

        b in ( field R) by A13, RELAT_1: 15;

        then b in (( field R) \ Y) by A14, XBOOLE_0:def 5;

        then

         A15: [a, b] in R by A10;

        b <> a by A12, Th1;

        hence contradiction by A1, A13, A15, Lm3;

      end;

      take a;

      thus a in ( field R) by A9;

      now

        

         A16: not a in Y by A9, XBOOLE_0:def 5;

        let b be object;

        assume

         A17: b in Y;

        assume not b in (R -Seg a);

        then

         A18: not [b, a] in R or a = b by Th1;

        a <> b by A9, A17, XBOOLE_0:def 5;

        then [a, b] in R by A2, A1, A9, A17, A18, Lm4;

        hence contradiction by A8, A17, A16;

      end;

      hence Y = (R -Seg a) by A11, TARSKI: 2;

    end;

    theorem :: WELLORD1:29

    

     Th29: R is well-ordering & a in ( field R) & b in ( field R) implies ( [a, b] in R iff (R -Seg a) c= (R -Seg b))

    proof

      assume that

       A1: R is well-ordering and

       A2: a in ( field R) and

       A3: b in ( field R);

      thus [a, b] in R implies (R -Seg a) c= (R -Seg b)

      proof

        assume

         A4: [a, b] in R;

        let c be object;

        assume

         A5: c in (R -Seg a);

        then

         A6: [c, a] in R by Th1;

        then

         A7: [c, b] in R by A1, A4, Lm2;

        c <> a by A5, Th1;

        then c <> b by A1, A4, A6, Lm3;

        hence thesis by A7, Th1;

      end;

      assume

       A8: (R -Seg a) c= (R -Seg b);

      now

        assume

         A9: a <> b;

        assume not [a, b] in R;

        then [b, a] in R by A2, A3, A1, A9, Lm4;

        then b in (R -Seg a) by A9, Th1;

        hence contradiction by A8, Th1;

      end;

      hence thesis by A1, A2, Lm1;

    end;

    theorem :: WELLORD1:30

    

     Th30: R is well-ordering & a in ( field R) & b in ( field R) implies ((R -Seg a) c= (R -Seg b) iff a = b or a in (R -Seg b))

    proof

      assume

       A1: R is well-ordering & a in ( field R) & b in ( field R);

      thus (R -Seg a) c= (R -Seg b) implies a = b or a in (R -Seg b)

      proof

        assume (R -Seg a) c= (R -Seg b);

        then [a, b] in R by A1, Th29;

        hence thesis by Th1;

      end;

      now

        assume a in (R -Seg b);

        then [a, b] in R by Th1;

        hence (R -Seg a) c= (R -Seg b) by A1, Th29;

      end;

      hence thesis;

    end;

    theorem :: WELLORD1:31

    

     Th31: R is well-ordering & X c= ( field R) implies ( field (R |_2 X)) = X

    proof

      assume that

       A1: R is well-ordering and

       A2: X c= ( field R);

      thus ( field (R |_2 X)) c= X by Th13;

      let x be object;

      assume

       A3: x in X;

      then

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

       [x, x] in R by A1, A2, A3, Lm1;

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

      hence thesis by RELAT_1: 15;

    end;

    theorem :: WELLORD1:32

    

     Th32: R is well-ordering implies ( field (R |_2 (R -Seg a))) = (R -Seg a)

    proof

      (R -Seg a) c= ( field R) by Th9;

      hence thesis by Th31;

    end;

    theorem :: WELLORD1:33

    

     Th33: R is well-ordering implies for Z st for a st a in ( field R) & (R -Seg a) c= Z holds a in Z holds ( field R) c= Z

    proof

      assume

       A1: R is well-ordering;

      let Z such that

       A2: for a st a in ( field R) & (R -Seg a) c= Z holds a in Z;

       A3:

      now

        let a such that

         A4: a in ( field R) and

         A5: for b st [b, a] in R & a <> b holds b in Z;

        now

          let b be object;

          assume b in (R -Seg a);

          then [b, a] in R & b <> a by Th1;

          hence b in Z by A5;

        end;

        then (R -Seg a) c= Z;

        hence a in Z by A2, A4;

      end;

      given a be object such that

       A6: a in ( field R) & not a in Z;

      (( field R) \ Z) <> {} by A6, XBOOLE_0:def 5;

      then

      consider a such that

       A7: a in (( field R) \ Z) and

       A8: for b st b in (( field R) \ Z) holds [a, b] in R by A1, Th6;

       not a in Z by A7, XBOOLE_0:def 5;

      then

      consider b such that

       A9: [b, a] in R and

       A10: b <> a and

       A11: not b in Z by A3, A7;

      b in ( field R) by A9, RELAT_1: 15;

      then b in (( field R) \ Z) by A11, XBOOLE_0:def 5;

      then [a, b] in R by A8;

      hence contradiction by A1, A9, A10, Lm3;

    end;

    theorem :: WELLORD1:34

    

     Th34: R is well-ordering & a in ( field R) & b in ( field R) & (for c st c in (R -Seg a) holds [c, b] in R & c <> b) implies [a, b] in R

    proof

      assume that

       A1: R is well-ordering & a in ( field R) & b in ( field R) and

       A2: c in (R -Seg a) implies [c, b] in R & c <> b;

      assume

       A3: not [a, b] in R;

      a <> b by A1, A3, Lm1;

      then [b, a] in R by A1, A3, Lm4;

      then b in (R -Seg a) by A3, Th1;

      hence contradiction by A2;

    end;

    theorem :: WELLORD1:35

    

     Th35: R is well-ordering & ( dom F) = ( field R) & ( rng F) c= ( field R) & (for a, b st [a, b] in R & a <> b holds [(F . a), (F . b)] in R & (F . a) <> (F . b)) implies for a st a in ( field R) holds [a, (F . a)] in R

    proof

      assume that

       A1: R is well-ordering & ( dom F) = ( field R) & ( rng F) c= ( field R) and

       A2: [a, b] in R & a <> b implies [(F . a), (F . b)] in R & (F . a) <> (F . b);

      defpred P[ object] means [$1, (F . $1)] in R;

      consider Z such that

       A3: for a be object holds a in Z iff a in ( field R) & P[a] from XBOOLE_0:sch 1;

      now

        let a;

        assume

         A4: a in ( field R);

        assume

         A5: (R -Seg a) c= Z;

         A6:

        now

          let b;

          assume

           A7: b in (R -Seg a);

          then

           A8: [b, (F . b)] in R by A3, A5;

          

           A9: [b, a] in R & b <> a by A7, Th1;

          then

           A10: [(F . b), (F . a)] in R by A2;

          hence [b, (F . a)] in R by A1, A8, Lm2;

          (F . b) <> (F . a) by A2, A9;

          hence b <> (F . a) by A1, A8, A10, Lm3;

        end;

        (F . a) in ( rng F) by A1, A4, FUNCT_1:def 3;

        then [a, (F . a)] in R by A1, A4, A6, Th34;

        hence a in Z by A3, A4;

      end;

      then

       A11: ( field R) c= Z by A1, Th33;

      let a;

      assume a in ( field R);

      hence thesis by A3, A11;

    end;

    definition

      let R, S, F;

      :: WELLORD1:def7

      pred F is_isomorphism_of R,S means ( dom F) = ( field R) & ( rng F) = ( field S) & F is one-to-one & for a, b holds [a, b] in R iff a in ( field R) & b in ( field R) & [(F . a), (F . b)] in S;

    end

    theorem :: WELLORD1:36

    

     Th36: F is_isomorphism_of (R,S) implies for a, b st [a, b] in R & a <> b holds [(F . a), (F . b)] in S & (F . a) <> (F . b)

    proof

      assume

       A1: F is_isomorphism_of (R,S);

      then

       A2: ( dom F) = ( field R) & F is one-to-one;

      let a, b;

      assume that

       A3: [a, b] in R and

       A4: a <> b;

      a in ( field R) & b in ( field R) by A1, A3;

      hence thesis by A1, A2, A3, A4;

    end;

    definition

      let R, S;

      :: WELLORD1:def8

      pred R,S are_isomorphic means ex F st F is_isomorphism_of (R,S);

    end

    theorem :: WELLORD1:37

    

     Th37: ( id ( field R)) is_isomorphism_of (R,R)

    proof

       A1:

      now

        let a, b;

        thus [a, b] in R implies a in ( field R) & b in ( field R) & [(( id ( field R)) . a), (( id ( field R)) . b)] in R

        proof

          assume

           A2: [a, b] in R;

          hence

           A3: a in ( field R) & b in ( field R) by RELAT_1: 15;

          then (( id ( field R)) . a) = a by FUNCT_1: 18;

          hence thesis by A2, A3, FUNCT_1: 18;

        end;

        assume that

         A4: a in ( field R) and

         A5: b in ( field R) & [(( id ( field R)) . a), (( id ( field R)) . b)] in R;

        (( id ( field R)) . a) = a by A4, FUNCT_1: 18;

        hence [a, b] in R by A5, FUNCT_1: 18;

      end;

      thus thesis by A1;

    end;

    theorem :: WELLORD1:38

    (R,R) are_isomorphic

    proof

      take ( id ( field R));

      thus thesis by Th37;

    end;

    theorem :: WELLORD1:39

    

     Th39: F is_isomorphism_of (R,S) implies (F " ) is_isomorphism_of (S,R)

    proof

      assume

       A1: F is_isomorphism_of (R,S);

      then

       A2: F is one-to-one;

      

       A3: ( rng F) = ( field S) by A1;

      hence

       A4: ( dom (F " )) = ( field S) by A2, FUNCT_1: 33;

      ( dom F) = ( field R) by A1;

      hence ( rng (F " )) = ( field R) by A2, FUNCT_1: 33;

      thus (F " ) is one-to-one by A2;

      let a, b;

      thus [a, b] in S implies a in ( field S) & b in ( field S) & [((F " ) . a), ((F " ) . b)] in R

      proof

        

         A5: ( dom F) = ( rng (F " )) by A2, FUNCT_1: 33;

        assume

         A6: [a, b] in S;

        hence

         A7: a in ( field S) & b in ( field S) by RELAT_1: 15;

        then

         A8: ((F " ) . a) in ( rng (F " )) & ((F " ) . b) in ( rng (F " )) by A4, FUNCT_1:def 3;

        a = (F . ((F " ) . a)) & b = (F . ((F " ) . b)) by A3, A2, A7, FUNCT_1: 35;

        hence thesis by A1, A6, A5, A8;

      end;

      assume that

       A9: a in ( field S) & b in ( field S) and

       A10: [((F " ) . a), ((F " ) . b)] in R;

      (F . ((F " ) . a)) = a & (F . ((F " ) . b)) = b by A3, A2, A9, FUNCT_1: 35;

      hence thesis by A1, A10;

    end;

    theorem :: WELLORD1:40

    

     Th40: (R,S) are_isomorphic implies (S,R) are_isomorphic

    proof

      given F such that

       A1: F is_isomorphism_of (R,S);

      take (F " );

      thus thesis by A1, Th39;

    end;

    theorem :: WELLORD1:41

    

     Th41: F is_isomorphism_of (R,S) & G is_isomorphism_of (S,T) implies (G * F) is_isomorphism_of (R,T)

    proof

      assume that

       A1: ( dom F) = ( field R) and

       A2: ( rng F) = ( field S) and

       A3: F is one-to-one and

       A4: for a, b holds [a, b] in R iff a in ( field R) & b in ( field R) & [(F . a), (F . b)] in S;

      assume that

       A5: ( dom G) = ( field S) and

       A6: ( rng G) = ( field T) and

       A7: G is one-to-one and

       A8: for a, b holds [a, b] in S iff a in ( field S) & b in ( field S) & [(G . a), (G . b)] in T;

      thus ( dom (G * F)) = ( field R) by A1, A2, A5, RELAT_1: 27;

      thus ( rng (G * F)) = ( field T) by A2, A5, A6, RELAT_1: 28;

      thus (G * F) is one-to-one by A3, A7;

      let a, b;

      thus [a, b] in R implies a in ( field R) & b in ( field R) & [((G * F) . a), ((G * F) . b)] in T

      proof

        assume

         A9: [a, b] in R;

        hence a in ( field R) & b in ( field R) by RELAT_1: 15;

        then

         A10: ((G * F) . a) = (G . (F . a)) & ((G * F) . b) = (G . (F . b)) by A1, FUNCT_1: 13;

         [(F . a), (F . b)] in S by A4, A9;

        hence thesis by A8, A10;

      end;

      assume that

       A11: a in ( field R) & b in ( field R) and

       A12: [((G * F) . a), ((G * F) . b)] in T;

      

       A13: ((G * F) . a) = (G . (F . a)) & ((G * F) . b) = (G . (F . b)) by A1, A11, FUNCT_1: 13;

      (F . a) in ( field S) & (F . b) in ( field S) by A1, A2, A11, FUNCT_1:def 3;

      then [(F . a), (F . b)] in S by A8, A12, A13;

      hence thesis by A4, A11;

    end;

    theorem :: WELLORD1:42

    

     Th42: (R,S) are_isomorphic & (S,T) are_isomorphic implies (R,T) are_isomorphic

    proof

      given F such that

       A1: F is_isomorphism_of (R,S);

      given G such that

       A2: G is_isomorphism_of (S,T);

      take (G * F);

      thus thesis by A1, A2, Th41;

    end;

    theorem :: WELLORD1:43

    

     Th43: F is_isomorphism_of (R,S) implies (R is reflexive implies S is reflexive) & (R is transitive implies S is transitive) & (R is connected implies S is connected) & (R is antisymmetric implies S is antisymmetric) & (R is well_founded implies S is well_founded)

    proof

      assume

       A1: F is_isomorphism_of (R,S);

      then

       A2: ( dom F) = ( field R);

      

       A3: ( rng F) = ( field S) by A1;

      

       A4: F is one-to-one by A1;

      then

       A5: ( rng (F " )) = ( dom F) & ( dom (F " )) = ( rng F) by FUNCT_1: 33;

      thus R is reflexive implies S is reflexive

      proof

        assume

         A6: R is reflexive;

        now

          let a;

          assume

           A7: a in ( field S);

          then ((F " ) . a) in ( field R) by A2, A3, A5, FUNCT_1:def 3;

          then

           A8: [((F " ) . a), ((F " ) . a)] in R by A6, Lm1;

          a = (F . ((F " ) . a)) by A3, A4, A7, FUNCT_1: 35;

          hence [a, a] in S by A1, A8;

        end;

        hence thesis by Lm1;

      end;

      thus R is transitive implies S is transitive

      proof

        assume

         A9: R is transitive;

        now

          let a, b, c;

          assume that

           A10: [a, b] in S and

           A11: [b, c] in S;

          

           A12: c in ( field S) by A11, RELAT_1: 15;

          then

           A13: c = (F . ((F " ) . c)) by A3, A4, FUNCT_1: 35;

          b in ( field S) by A10, RELAT_1: 15;

          then

           A14: b = (F . ((F " ) . b)) & ((F " ) . b) in ( field R) by A2, A3, A4, A5, FUNCT_1: 35, FUNCT_1:def 3;

          ((F " ) . c) in ( field R) by A2, A3, A5, A12, FUNCT_1:def 3;

          then

           A15: [((F " ) . b), ((F " ) . c)] in R by A1, A11, A13, A14;

          

           A16: a in ( field S) by A10, RELAT_1: 15;

          then

           A17: a = (F . ((F " ) . a)) by A3, A4, FUNCT_1: 35;

          ((F " ) . a) in ( field R) by A2, A3, A5, A16, FUNCT_1:def 3;

          then [((F " ) . a), ((F " ) . b)] in R by A1, A10, A17, A14;

          then [((F " ) . a), ((F " ) . c)] in R by A9, A15, Lm2;

          hence [a, c] in S by A1, A17, A13;

        end;

        hence thesis by Lm2;

      end;

      thus R is connected implies S is connected

      proof

        assume

         A18: R is connected;

        now

          let a, b;

          assume that

           A19: a in ( field S) & b in ( field S) and

           A20: a <> b;

          

           A21: a = (F . ((F " ) . a)) & b = (F . ((F " ) . b)) by A3, A4, A19, FUNCT_1: 35;

          ((F " ) . a) in ( field R) & ((F " ) . b) in ( field R) by A2, A3, A5, A19, FUNCT_1:def 3;

          then [((F " ) . a), ((F " ) . b)] in R or [((F " ) . b), ((F " ) . a)] in R by A18, A20, A21, Lm4;

          hence [a, b] in S or [b, a] in S by A1, A21;

        end;

        hence thesis by Lm4;

      end;

      thus R is antisymmetric implies S is antisymmetric

      proof

        assume

         A22: R is antisymmetric;

        now

          let a, b;

          assume that

           A23: [a, b] in S and

           A24: [b, a] in S;

          

           A25: a in ( field S) by A23, RELAT_1: 15;

          then

           A26: a = (F . ((F " ) . a)) by A3, A4, FUNCT_1: 35;

          

           A27: b in ( field S) by A23, RELAT_1: 15;

          then

           A28: b = (F . ((F " ) . b)) by A3, A4, FUNCT_1: 35;

          

           A29: ((F " ) . b) in ( field R) by A2, A3, A5, A27, FUNCT_1:def 3;

          ((F " ) . a) in ( field R) by A2, A3, A5, A25, FUNCT_1:def 3;

          then [((F " ) . a), ((F " ) . b)] in R & [((F " ) . b), ((F " ) . a)] in R by A1, A23, A24, A26, A28, A29;

          hence a = b by A22, A26, A28, Lm3;

        end;

        hence thesis by Lm3;

      end;

      assume

       A30: for Y st Y c= ( field R) & Y <> {} holds ex x st x in Y & (R -Seg x) misses Y;

      let Z;

      assume that

       A31: Z c= ( field S) and

       A32: Z <> {} ;

      

       A33: (F " Z) c= ( dom F) by RELAT_1: 132;

      then

      consider x such that

       A34: x in (F " Z) and

       A35: (R -Seg x) misses (F " Z) by A2, A3, A30, A31, A32, RELAT_1: 139;

      take (F . x);

      thus (F . x) in Z by A34, FUNCT_1:def 7;

      assume not thesis;

      then

      consider y be object such that

       A36: y in (S -Seg (F . x)) and

       A37: y in Z by XBOOLE_0: 3;

      

       A38: ((F " ) . y) in ( dom F) by A3, A5, A31, A37, FUNCT_1:def 3;

      

       A39: [y, (F . x)] in S by A36, Th1;

      

       A40: y = (F . ((F " ) . y)) by A3, A4, A31, A37, FUNCT_1: 35;

      then ((F " ) . y) in (F " Z) by A37, A38, FUNCT_1:def 7;

      then not ((F " ) . y) in (R -Seg x) by A35, XBOOLE_0: 3;

      then not [((F " ) . y), x] in R or ((F " ) . y) = x by Th1;

      hence contradiction by A1, A33, A34, A36, A40, A38, A39, Th1;

    end;

    theorem :: WELLORD1:44

    

     Th44: R is well-ordering & F is_isomorphism_of (R,S) implies S is well-ordering by Th43;

    theorem :: WELLORD1:45

    

     Th45: R is well-ordering implies for F, G st F is_isomorphism_of (R,S) & G is_isomorphism_of (R,S) holds F = G

    proof

      assume

       A1: R is well-ordering;

      let F, G;

      assume that

       A2: F is_isomorphism_of (R,S) and

       A3: G is_isomorphism_of (R,S);

      

       A4: ( dom F) = ( field R) by A2;

      

       A5: S is well-ordering by A1, A2, Th44;

      

       A6: ( rng F) = ( field S) by A2;

      

       A7: G is one-to-one by A3;

      

       A8: ( dom G) = ( field R) by A3;

      

       A9: (G " ) is_isomorphism_of (S,R) by A3, Th39;

      then

       A10: (G " ) is one-to-one;

      

       A11: F is one-to-one by A2;

      

       A12: ( rng G) = ( field S) by A3;

      

       A13: (F " ) is_isomorphism_of (S,R) by A2, Th39;

      then

       A14: (F " ) is one-to-one;

      for a be object st a in ( field R) holds (F . a) = (G . a)

      proof

        

         A15: ( dom (F " )) = ( field S) by A6, A11, FUNCT_1: 33;

        then

         A16: ( dom ((F " ) * G)) = ( field R) by A8, A12, RELAT_1: 27;

         A17:

        now

          let a, b;

          assume that

           A18: [a, b] in R and

           A19: a <> b;

          

           A20: [(G . a), (G . b)] in S by A3, A18;

          

           A21: b in ( field R) by A18, RELAT_1: 15;

          then

           A22: ((F " ) . (G . b)) = (((F " ) * G) . b) by A8, FUNCT_1: 13;

          

           A23: a in ( field R) by A18, RELAT_1: 15;

          then ((F " ) . (G . a)) = (((F " ) * G) . a) by A8, FUNCT_1: 13;

          hence [(((F " ) * G) . a), (((F " ) * G) . b)] in R by A13, A20, A22;

          thus (((F " ) * G) . a) <> (((F " ) * G) . b) by A14, A7, A16, A19, A23, A21, FUNCT_1:def 4;

        end;

        

         A24: ( dom (G " )) = ( field S) by A12, A7, FUNCT_1: 33;

        then

         A25: ( dom ((G " ) * F)) = ( field R) by A4, A6, RELAT_1: 27;

         A26:

        now

          let a, b;

          assume that

           A27: [a, b] in R and

           A28: a <> b;

          

           A29: [(F . a), (F . b)] in S by A2, A27;

          

           A30: b in ( field R) by A27, RELAT_1: 15;

          then

           A31: ((G " ) . (F . b)) = (((G " ) * F) . b) by A4, FUNCT_1: 13;

          

           A32: a in ( field R) by A27, RELAT_1: 15;

          then ((G " ) . (F . a)) = (((G " ) * F) . a) by A4, FUNCT_1: 13;

          hence [(((G " ) * F) . a), (((G " ) * F) . b)] in R by A9, A29, A31;

          thus (((G " ) * F) . a) <> (((G " ) * F) . b) by A11, A10, A25, A28, A32, A30, FUNCT_1:def 4;

        end;

        let a be object such that

         A33: a in ( field R);

        

         A34: ((F " ) . (G . a)) = (((F " ) * G) . a) by A8, A33, FUNCT_1: 13;

        (G . a) in ( rng F) by A6, A8, A12, A33, FUNCT_1:def 3;

        then

         A35: (F . ((F " ) . (G . a))) = (G . a) by A11, FUNCT_1: 35;

        ( rng (F " )) = ( field R) by A4, A11, FUNCT_1: 33;

        then ( rng ((F " ) * G)) = ( field R) by A12, A15, RELAT_1: 28;

        then [a, (((F " ) * G) . a)] in R by A1, A33, A16, A17, Th35;

        then

         A36: [(F . a), (G . a)] in S by A2, A34, A35;

        (F . a) in ( rng G) by A4, A6, A12, A33, FUNCT_1:def 3;

        then

         A37: (G . ((G " ) . (F . a))) = (F . a) by A7, FUNCT_1: 35;

        

         A38: ((G " ) . (F . a)) = (((G " ) * F) . a) by A4, A33, FUNCT_1: 13;

        ( rng (G " )) = ( field R) by A8, A7, FUNCT_1: 33;

        then ( rng ((G " ) * F)) = ( field R) by A6, A24, RELAT_1: 28;

        then [a, (((G " ) * F) . a)] in R by A1, A33, A25, A26, Th35;

        then [(G . a), (F . a)] in S by A3, A38, A37;

        hence thesis by A5, A36, Lm3;

      end;

      hence thesis by A4, A8;

    end;

    definition

      let R, S;

      assume that

       A1: R is well-ordering and

       A2: (R,S) are_isomorphic ;

      :: WELLORD1:def9

      func canonical_isomorphism_of (R,S) -> Function means

      : Def9: it is_isomorphism_of (R,S);

      existence by A2;

      uniqueness by A1, Th45;

    end

    theorem :: WELLORD1:46

    

     Th46: R is well-ordering implies for a st a in ( field R) holds not (R,(R |_2 (R -Seg a))) are_isomorphic

    proof

      assume

       A1: R is well-ordering;

      let a such that

       A2: a in ( field R);

      set S = (R |_2 (R -Seg a));

      set F = ( canonical_isomorphism_of (R,S));

      assume (R,(R |_2 (R -Seg a))) are_isomorphic ;

      then

       A3: F is_isomorphism_of (R,S) by A1, Def9;

      then

       A4: ( dom F) = ( field R);

      

       A5: F is one-to-one by A3;

       A6:

      now

        let b, c;

        assume that

         A7: [b, c] in R and

         A8: b <> c;

         [(F . b), (F . c)] in (R |_2 (R -Seg a)) by A3, A7;

        hence [(F . b), (F . c)] in R by XBOOLE_0:def 4;

        b in ( field R) & c in ( field R) by A7, RELAT_1: 15;

        hence (F . b) <> (F . c) by A4, A5, A8;

      end;

      

       A9: ( rng F) = ( field S) by A3;

      ( field S) = (R -Seg a) by A1, Th32;

      then (F . a) in (R -Seg a) by A2, A4, A9, FUNCT_1:def 3;

      then

       A10: [(F . a), a] in R & (F . a) <> a by Th1;

      ( rng F) c= ( field R) by A9, Th13;

      then [a, (F . a)] in R by A1, A2, A4, A6, Th35;

      hence contradiction by A1, A10, Lm3;

    end;

    theorem :: WELLORD1:47

    

     Th47: R is well-ordering & a in ( field R) & b in ( field R) & a <> b implies not ((R |_2 (R -Seg a)),(R |_2 (R -Seg b))) are_isomorphic

    proof

      assume that

       A1: R is well-ordering and

       A2: a in ( field R) & b in ( field R) and

       A3: a <> b;

       A4:

      now

        set S = (R |_2 (R -Seg a));

        assume

         A5: (R -Seg b) c= (R -Seg a);

        then

         A6: (S |_2 (R -Seg b)) = (R |_2 (R -Seg b)) by Th22;

        

         A7: ( field S) = (R -Seg a) by A1, Th32;

        

         A8: b in (R -Seg a)

        proof

          assume not b in (R -Seg a);

          then not [b, a] in R by A3, Th1;

          then [a, b] in R by A2, A3, A1, Lm4;

          then a in (R -Seg b) by A3, Th1;

          hence contradiction by A5, Th1;

        end;

        then (R -Seg b) = (S -Seg b) by A1, Th27;

        hence thesis by A1, A7, A8, A6, Th25, Th46;

      end;

       A9:

      now

        set S = (R |_2 (R -Seg b));

        assume

         A10: (R -Seg a) c= (R -Seg b);

        then

         A11: (S |_2 (R -Seg a)) = (R |_2 (R -Seg a)) by Th22;

        

         A12: ( field S) = (R -Seg b) & S is well-ordering by A1, Th25, Th32;

        

         A13: a in (R -Seg b)

        proof

          assume not a in (R -Seg b);

          then not [a, b] in R by A3, Th1;

          then [b, a] in R by A2, A3, A1, Lm4;

          then b in (R -Seg a) by A3, Th1;

          hence contradiction by A10, Th1;

        end;

        then (R -Seg a) = (S -Seg a) by A1, Th27;

        hence thesis by A13, A11, A12, Th40, Th46;

      end;

      ((R -Seg a),(R -Seg b)) are_c=-comparable by A1, Th26;

      hence thesis by A9, A4;

    end;

    theorem :: WELLORD1:48

    

     Th48: R is well-ordering & Z c= ( field R) & F is_isomorphism_of (R,S) implies (F | Z) is_isomorphism_of ((R |_2 Z),(S |_2 (F .: Z))) & ((R |_2 Z),(S |_2 (F .: Z))) are_isomorphic

    proof

      assume that

       A1: R is well-ordering and

       A2: Z c= ( field R) and

       A3: F is_isomorphism_of (R,S);

      

       A4: (F .: Z) c= ( rng F) by RELAT_1: 111;

      

       A5: (F .: Z) = ( field (S |_2 (F .: Z))) by A1, A3, A4, Th31, Th44;

      

       A6: F is one-to-one by A3;

      

       A7: Z = ( field (R |_2 Z)) by A1, A2, Th31;

      

       A8: ( dom F) = ( field R) by A3;

      thus (F | Z) is_isomorphism_of ((R |_2 Z),(S |_2 (F .: Z)))

      proof

        thus

         A9: ( dom (F | Z)) = ( field (R |_2 Z)) by A2, A8, A7, RELAT_1: 62;

        thus

         A10: ( rng (F | Z)) = ( field (S |_2 (F .: Z))) by A5, RELAT_1: 115;

        thus (F | Z) is one-to-one by A6, FUNCT_1: 52;

        let a, b;

        thus [a, b] in (R |_2 Z) implies a in ( field (R |_2 Z)) & b in ( field (R |_2 Z)) & [((F | Z) . a), ((F | Z) . b)] in (S |_2 (F .: Z))

        proof

          assume

           A11: [a, b] in (R |_2 Z);

          then [a, b] in R by XBOOLE_0:def 4;

          then

           A12: [(F . a), (F . b)] in S by A3;

          thus

           A13: a in ( field (R |_2 Z)) & b in ( field (R |_2 Z)) by A11, RELAT_1: 15;

          then ((F | Z) . a) in ( rng (F | Z)) & ((F | Z) . b) in ( rng (F | Z)) by A9, FUNCT_1:def 3;

          then

           A14: [((F | Z) . a), ((F | Z) . b)] in [:(F .: Z), (F .: Z):] by A5, A10, ZFMISC_1: 87;

          (F . a) = ((F | Z) . a) & (F . b) = ((F | Z) . b) by A9, A13, FUNCT_1: 47;

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

        end;

        assume that

         A15: a in ( field (R |_2 Z)) & b in ( field (R |_2 Z)) and

         A16: [((F | Z) . a), ((F | Z) . b)] in (S |_2 (F .: Z));

        (F . a) = ((F | Z) . a) & (F . b) = ((F | Z) . b) by A9, A15, FUNCT_1: 47;

        then

         A17: [(F . a), (F . b)] in S by A16, XBOOLE_0:def 4;

        

         A18: [a, b] in [:Z, Z:] by A7, A15, ZFMISC_1: 87;

        a in ( field R) & b in ( field R) by A15, Th12;

        then [a, b] in R by A3, A17;

        hence thesis by A18, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: WELLORD1:49

    

     Th49: F is_isomorphism_of (R,S) implies for a st a in ( field R) holds ex b st b in ( field S) & (F .: (R -Seg a)) = (S -Seg b)

    proof

      assume

       A1: F is_isomorphism_of (R,S);

      then

       A2: ( dom F) = ( field R);

      let a;

      assume

       A3: a in ( field R);

      take b = (F . a);

      

       A4: ( rng F) = ( field S) by A1;

      hence b in ( field S) by A3, A2, FUNCT_1:def 3;

      

       A5: F is one-to-one by A1;

      

       A6: for c be object holds c in (S -Seg b) implies c in (F .: (R -Seg a))

      proof

        let c be object;

        assume

         A7: c in (S -Seg b);

        then

         A8: c <> b by Th1;

        

         A9: [c, b] in S by A7, Th1;

        then

         A10: c in ( field S) by RELAT_1: 15;

        then

         A11: c = (F . ((F " ) . c)) by A4, A5, FUNCT_1: 35;

        ( rng (F " )) = ( dom F) & ( dom (F " )) = ( rng F) by A5, FUNCT_1: 33;

        then

         A12: ((F " ) . c) in ( field R) by A2, A4, A10, FUNCT_1:def 3;

        then [((F " ) . c), a] in R by A1, A3, A9, A11;

        then ((F " ) . c) in (R -Seg a) by A8, A11, Th1;

        hence thesis by A2, A11, A12, FUNCT_1:def 6;

      end;

      for c be object holds c in (F .: (R -Seg a)) implies c in (S -Seg b)

      proof

        let c be object;

        assume c in (F .: (R -Seg a));

        then

        consider d be object such that

         A13: d in ( dom F) and

         A14: d in (R -Seg a) and

         A15: c = (F . d) by FUNCT_1:def 6;

         [d, a] in R by A14, Th1;

        then

         A16: [c, b] in S by A1, A15;

        d <> a by A14, Th1;

        then c <> b by A3, A2, A5, A13, A15;

        hence thesis by A16, Th1;

      end;

      hence thesis by A6, TARSKI: 2;

    end;

    theorem :: WELLORD1:50

    

     Th50: R is well-ordering & F is_isomorphism_of (R,S) implies for a st a in ( field R) holds ex b st b in ( field S) & ((R |_2 (R -Seg a)),(S |_2 (S -Seg b))) are_isomorphic

    proof

      assume that

       A1: R is well-ordering and

       A2: F is_isomorphism_of (R,S);

      let a;

      assume a in ( field R);

      then

      consider b such that

       A3: b in ( field S) & (F .: (R -Seg a)) = (S -Seg b) by A2, Th49;

      take b;

      (R -Seg a) c= ( field R) by Th9;

      hence thesis by A1, A2, A3, Th48;

    end;

    theorem :: WELLORD1:51

    

     Th51: R is well-ordering & S is well-ordering & a in ( field R) & b in ( field S) & c in ( field S) & (R,(S |_2 (S -Seg b))) are_isomorphic & ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) are_isomorphic implies (S -Seg c) c= (S -Seg b) & [c, b] in S

    proof

      assume that

       A1: R is well-ordering and

       A2: S is well-ordering and

       A3: a in ( field R) and

       A4: b in ( field S) and

       A5: c in ( field S) and

       A6: (R,(S |_2 (S -Seg b))) are_isomorphic and

       A7: ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) are_isomorphic ;

      set Q = (S |_2 (S -Seg b));

      set F1 = ( canonical_isomorphism_of (R,Q));

      

       A8: F1 is_isomorphism_of (R,Q) by A1, A6, Def9;

      then

      consider d such that

       A9: d in ( field Q) and

       A10: (F1 .: (R -Seg a)) = (Q -Seg d) by A3, Th49;

      

       A11: (S -Seg b) = ( field Q) by A2, Th32;

      then

       A12: (Q -Seg d) = (S -Seg d) by A2, A9, Th27;

      

       A13: ( rng F1) = (S -Seg b) by A8, A11;

      then

       A14: (Q -Seg d) c= (S -Seg b) by A10, RELAT_1: 111;

      set T = (S |_2 (S -Seg c));

      set P = (R |_2 (R -Seg a));

      

       A15: (T,P) are_isomorphic by A7, Th40;

      

       A16: d in ( field S) by A9, Th12;

      (R -Seg a) c= ( field R) by Th9;

      then (P,(Q |_2 (F1 .: (R -Seg a)))) are_isomorphic by A1, A8, Th48;

      then (T,(Q |_2 (Q -Seg d))) are_isomorphic by A10, A15, Th42;

      then (T,(S |_2 (S -Seg d))) are_isomorphic by A10, A12, A13, Th22, RELAT_1: 111;

      hence (S -Seg c) c= (S -Seg b) by A2, A5, A12, A14, A16, Th47;

      hence thesis by A2, A4, A5, Th29;

    end;

    theorem :: WELLORD1:52

    

     Th52: R is well-ordering & S is well-ordering implies (R,S) are_isomorphic or (ex a st a in ( field R) & ((R |_2 (R -Seg a)),S) are_isomorphic ) or ex a st a in ( field S) & (R,(S |_2 (S -Seg a))) are_isomorphic

    proof

      assume that

       A1: R is well-ordering and

       A2: S is well-ordering;

      defpred P[ object] means ex b st b in ( field S) & ((R |_2 (R -Seg $1)),(S |_2 (S -Seg b))) are_isomorphic ;

      consider Z such that

       A3: for a be object holds a in Z iff a in ( field R) & P[a] from XBOOLE_0:sch 1;

      

       A4: Z c= ( field R) by A3;

      defpred P[ object, object] means $2 in ( field S) & ((R |_2 (R -Seg $1)),(S |_2 (S -Seg $2))) are_isomorphic ;

      

       A5: for a,b,c be object st P[a, b] & P[a, c] holds b = c

      proof

        let a,b,c be object;

        assume that

         A6: b in ( field S) and

         A7: ((R |_2 (R -Seg a)),(S |_2 (S -Seg b))) are_isomorphic and

         A8: c in ( field S) & ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) are_isomorphic ;

        ((S |_2 (S -Seg b)),(R |_2 (R -Seg a))) are_isomorphic by A7, Th40;

        hence thesis by A2, A6, A8, Th42, Th47;

      end;

      consider F such that

       A9: for a,b be object holds [a, b] in F iff a in ( field R) & P[a, b] from FUNCT_1:sch 1( A5);

      

       A10: Z = ( dom F)

      proof

        thus for a be object holds a in Z implies a in ( dom F)

        proof

          let a be object;

          assume

           A11: a in Z;

          then

          consider b such that

           A12: b in ( field S) & ((R |_2 (R -Seg a)),(S |_2 (S -Seg b))) are_isomorphic by A3;

          a in ( field R) by A3, A11;

          then [a, b] in F by A9, A12;

          hence thesis by XTUPLE_0:def 12;

        end;

        let a be object;

        assume a in ( dom F);

        then

        consider b be object such that

         A13: [a, b] in F by XTUPLE_0:def 12;

        

         A14: ((R |_2 (R -Seg a)),(S |_2 (S -Seg b))) are_isomorphic by A9, A13;

        a in ( field R) & b in ( field S) by A9, A13;

        hence thesis by A3, A14;

      end;

      

       A15: ( rng F) c= ( field S)

      proof

        let a be object;

        assume a in ( rng F);

        then

        consider b be object such that

         A16: b in ( dom F) & a = (F . b) by FUNCT_1:def 3;

         [b, a] in F by A16, FUNCT_1: 1;

        hence thesis by A9;

      end;

      

       A17: F is_isomorphism_of ((R |_2 ( dom F)),(S |_2 ( rng F)))

      proof

        thus ( dom F) = ( field (R |_2 ( dom F))) & ( rng F) = ( field (S |_2 ( rng F))) by A1, A2, A4, A15, A10, Th31;

        thus

         A18: F is one-to-one

        proof

          let a,b be object;

          assume that

           A19: a in ( dom F) and

           A20: b in ( dom F) and

           A21: (F . a) = (F . b);

          

           A22: [b, (F . b)] in F by A20, FUNCT_1: 1;

          then ((R |_2 (R -Seg b)),(S |_2 (S -Seg (F . a)))) are_isomorphic by A9, A21;

          then

           A23: ((S |_2 (S -Seg (F . a))),(R |_2 (R -Seg b))) are_isomorphic by Th40;

           [a, (F . a)] in F by A19, FUNCT_1: 1;

          then

           A24: a in ( field R) & ((R |_2 (R -Seg a)),(S |_2 (S -Seg (F . a)))) are_isomorphic by A9;

          b in ( field R) by A9, A22;

          hence thesis by A1, A24, A23, Th42, Th47;

        end;

        let a, b;

        set P = (R |_2 (R -Seg a));

        

         A25: ( field P) = (R -Seg a) & P is well-ordering by A1, Th25, Th32;

        thus [a, b] in (R |_2 ( dom F)) implies a in ( field (R |_2 ( dom F))) & b in ( field (R |_2 ( dom F))) & [(F . a), (F . b)] in (S |_2 ( rng F))

        proof

          assume

           A26: [a, b] in (R |_2 ( dom F));

          hence

           A27: a in ( field (R |_2 ( dom F))) & b in ( field (R |_2 ( dom F))) by RELAT_1: 15;

          then

           A28: a in ( dom F) by Th12;

          then

           A29: [a, (F . a)] in F by FUNCT_1: 1;

          then

           A30: (F . a) in ( field S) by A9;

          

           A31: b in ( dom F) by A27, Th12;

          then

           A32: [b, (F . b)] in F by FUNCT_1: 1;

          then

           A33: b in ( field R) by A9;

          

           A34: (F . b) in ( field S) & ((R |_2 (R -Seg b)),(S |_2 (S -Seg (F . b)))) are_isomorphic by A9, A32;

          

           A35: [a, b] in R by A26, XBOOLE_0:def 4;

          

           A36: (F . b) in ( rng F) by A31, FUNCT_1:def 3;

          (F . a) in ( rng F) by A28, FUNCT_1:def 3;

          then

           A37: [(F . a), (F . b)] in [:( rng F), ( rng F):] by A36, ZFMISC_1: 87;

          a in ( field R) by A9, A29;

          then

           A38: (R -Seg a) c= (R -Seg b) by A1, A33, A35, Th29;

          

           A39: ((R |_2 (R -Seg a)),(S |_2 (S -Seg (F . a)))) are_isomorphic by A9, A29;

           A40:

          now

            set P = (R |_2 (R -Seg b));

            

             A41: ( field P) = (R -Seg b) & P is well-ordering by A1, Th25, Th32;

            assume a <> b;

            then

             A42: a in (R -Seg b) by A35, Th1;

            then (P -Seg a) = (R -Seg a) by A1, Th27;

            then ((P |_2 (P -Seg a)),(S |_2 (S -Seg (F . a)))) are_isomorphic by A39, A38, Th22;

            then [(F . a), (F . b)] in S by A2, A30, A34, A42, A41, Th51;

            hence thesis by A37, XBOOLE_0:def 4;

          end;

          a = b implies thesis

          proof

            assume a = b;

            then [(F . a), (F . b)] in S by A2, A30, Lm1;

            hence thesis by A37, XBOOLE_0:def 4;

          end;

          hence thesis by A40;

        end;

        assume that

         A43: a in ( field (R |_2 ( dom F))) and

         A44: b in ( field (R |_2 ( dom F))) and

         A45: [(F . a), (F . b)] in (S |_2 ( rng F));

        

         A46: [(F . a), (F . b)] in S by A45, XBOOLE_0:def 4;

        

         A47: a in ( dom F) by A43, Th12;

        then

         A48: [a, (F . a)] in F by FUNCT_1: 1;

        then

         A49: a in ( field R) by A9;

        assume not [a, b] in (R |_2 ( dom F));

        then

         A50: not [a, b] in R or not [a, b] in [:( dom F), ( dom F):] by XBOOLE_0:def 4;

        then

         A51: a <> b by A1, A47, A49, Lm1, ZFMISC_1: 87;

        

         A52: b in ( dom F) by A44, Th12;

        then

         A53: [b, (F . b)] in F by FUNCT_1: 1;

        then

         A54: ((R |_2 (R -Seg b)),(S |_2 (S -Seg (F . b)))) are_isomorphic by A9;

        

         A55: b in ( field R) by A9, A53;

        then

         A56: [b, a] in R by A1, A47, A52, A50, A49, A51, Lm4, ZFMISC_1: 87;

        then

         A57: (R -Seg b) c= (R -Seg a) by A1, A49, A55, Th29;

        

         A58: b in (R -Seg a) by A47, A52, A50, A56, Th1, ZFMISC_1: 87;

        then (P -Seg b) = (R -Seg b) by A1, Th27;

        then

         A59: ((P |_2 (P -Seg b)),(S |_2 (S -Seg (F . b)))) are_isomorphic by A54, A57, Th22;

        

         A60: (F . b) in ( field S) by A9, A53;

        (F . a) in ( field S) & ((R |_2 (R -Seg a)),(S |_2 (S -Seg (F . a)))) are_isomorphic by A9, A48;

        then [(F . b), (F . a)] in S by A2, A60, A58, A25, A59, Th51;

        then (F . a) = (F . b) by A2, A46, Lm3;

        hence contradiction by A18, A47, A52, A51;

      end;

       A61:

      now

        given a such that

         A62: a in ( field R) and

         A63: Z = (R -Seg a);

        given b such that

         A64: b in ( field S) and

         A65: ( rng F) = (S -Seg b);

        ((R |_2 (R -Seg a)),(S |_2 (S -Seg b))) are_isomorphic by A10, A17, A63, A65;

        then a in Z by A3, A62, A64;

        hence contradiction by A63, Th1;

      end;

       A66:

      now

        let a such that

         A67: a in Z;

        consider c such that

         A68: c in ( field S) and

         A69: ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) are_isomorphic by A3, A67;

        let b such that

         A70: [b, a] in R;

        

         A71: a in ( field R) by A3, A67;

        now

          set Q = (S |_2 (S -Seg c));

          set P = (R |_2 (R -Seg a));

          P is well-ordering by A1, Th25;

          then

           A72: ( canonical_isomorphism_of (P,Q)) is_isomorphism_of (P,Q) by A69, Def9;

          assume a <> b;

          then

           A73: b in (R -Seg a) by A70, Th1;

          then

           A74: (P -Seg b) = (R -Seg b) by A1, Th27;

          

           A75: b in ( field R) by A70, RELAT_1: 15;

          then (R -Seg b) c= (R -Seg a) by A1, A71, A73, Th30;

          then

           A76: (P |_2 (R -Seg b)) = (R |_2 (R -Seg b)) by Th22;

          ( field P) = (R -Seg a) by A1, Th32;

          then

          consider d such that

           A77: d in ( field Q) and

           A78: ((P |_2 (P -Seg b)),(Q |_2 (Q -Seg d))) are_isomorphic by A1, A72, A73, Th25, Th50;

          

           A79: (S -Seg c) = ( field Q) by A2, Th32;

          then

           A80: (Q -Seg d) = (S -Seg d) by A2, A77, Th27;

           [d, c] in S by A77, A79, Th1;

          then

           A81: d in ( field S) by RELAT_1: 15;

          then (S -Seg d) c= (S -Seg c) by A2, A68, A77, A79, Th30;

          then ((R |_2 (R -Seg b)),(S |_2 (S -Seg d))) are_isomorphic by A78, A74, A80, A76, Th22;

          hence b in Z by A3, A75, A81;

        end;

        hence b in Z by A67;

      end;

      

       A82: ((R |_2 Z),(S |_2 ( rng F))) are_isomorphic by A10, A17;

       A83:

      now

        assume

         A84: Z = ( field R);

        given a such that

         A85: a in ( field S) and

         A86: ( rng F) = (S -Seg a);

        take a;

        thus a in ( field S) by A85;

        thus (R,(S |_2 (S -Seg a))) are_isomorphic by A82, A84, A86, Th23;

      end;

       A87:

      now

        let a such that

         A88: a in ( rng F);

        consider c be object such that

         A89: c in ( dom F) & a = (F . c) by A88, FUNCT_1:def 3;

        

         A90: [c, a] in F by A89, FUNCT_1: 1;

        then

         A91: a in ( field S) by A9;

        let b such that

         A92: [b, a] in S;

        

         A93: ((R |_2 (R -Seg c)),(S |_2 (S -Seg a))) are_isomorphic by A9, A90;

        

         A94: c in ( field R) by A9, A90;

        now

          set Q = (S |_2 (S -Seg a));

          set P = (R |_2 (R -Seg c));

          assume a <> b;

          then

           A95: b in (S -Seg a) by A92, Th1;

          then

           A96: (Q -Seg b) = (S -Seg b) by A2, Th27;

          

           A97: b in ( field S) by A92, RELAT_1: 15;

          then (S -Seg b) c= (S -Seg a) by A2, A91, A95, Th30;

          then

           A98: (Q |_2 (S -Seg b)) = (S |_2 (S -Seg b)) by Th22;

          (Q,P) are_isomorphic & Q is well-ordering by A2, A93, Th25, Th40;

          then

           A99: ( canonical_isomorphism_of (Q,P)) is_isomorphism_of (Q,P) by Def9;

          ( field Q) = (S -Seg a) by A2, Th32;

          then

          consider d such that

           A100: d in ( field P) and

           A101: ((Q |_2 (Q -Seg b)),(P |_2 (P -Seg d))) are_isomorphic by A2, A99, A95, Th25, Th50;

          

           A102: (R -Seg c) = ( field P) by A1, Th32;

          then

           A103: (P -Seg d) = (R -Seg d) by A1, A100, Th27;

           [d, c] in R by A100, A102, Th1;

          then

           A104: d in ( field R) by RELAT_1: 15;

          then (R -Seg d) c= (R -Seg c) by A1, A94, A100, A102, Th30;

          then ((S |_2 (S -Seg b)),(R |_2 (R -Seg d))) are_isomorphic by A101, A96, A103, A98, Th22;

          then ((R |_2 (R -Seg d)),(S |_2 (S -Seg b))) are_isomorphic by Th40;

          then [d, b] in F by A9, A97, A104;

          then d in ( dom F) & b = (F . d) by FUNCT_1: 1;

          hence b in ( rng F) by FUNCT_1:def 3;

        end;

        hence b in ( rng F) by A88;

      end;

       A105:

      now

        assume

         A106: ( rng F) = ( field S);

        given a such that

         A107: a in ( field R) and

         A108: Z = (R -Seg a);

        take a;

        thus a in ( field R) by A107;

        thus ((R |_2 (R -Seg a)),S) are_isomorphic by A82, A106, A108, Th23;

      end;

      now

        assume

         A109: Z = ( field R) & ( rng F) = ( field S);

        (R |_2 ( field R)) = R & (S |_2 ( field S)) = S by Th23;

        hence (R,S) are_isomorphic by A10, A17, A109;

      end;

      hence thesis by A1, A2, A4, A15, A66, A87, A61, A83, A105, Th28;

    end;

    theorem :: WELLORD1:53

    Y c= ( field R) & R is well-ordering implies (R,(R |_2 Y)) are_isomorphic or ex a st a in ( field R) & ((R |_2 (R -Seg a)),(R |_2 Y)) are_isomorphic

    proof

      assume that

       A1: Y c= ( field R) and

       A2: R is well-ordering;

       A3:

      now

        given a such that

         A4: a in ( field (R |_2 Y)) and

         A5: (R,((R |_2 Y) |_2 ((R |_2 Y) -Seg a))) are_isomorphic ;

        consider F such that

         A6: F is_isomorphism_of (R,((R |_2 Y) |_2 ((R |_2 Y) -Seg a))) by A5;

         A7:

        now

          let c, b;

          assume

           A8: [c, b] in R & c <> b;

          then [(F . c), (F . b)] in ((R |_2 Y) |_2 ((R |_2 Y) -Seg a)) by A6;

          then [(F . c), (F . b)] in (R |_2 Y) by XBOOLE_0:def 4;

          hence [(F . c), (F . b)] in R & (F . c) <> (F . b) by A6, A8, Th36, XBOOLE_0:def 4;

        end;

        

         A9: ( field (R |_2 Y)) = Y by A1, A2, Th31;

        ( field ((R |_2 Y) |_2 ((R |_2 Y) -Seg a))) = ((R |_2 Y) -Seg a) by A2, Th25, Th32;

        then

         A10: ( rng F) = ((R |_2 Y) -Seg a) by A6;

        

         A11: ( dom F) = ( field R) by A6;

        then

         A12: (F . a) in ( rng F) by A1, A4, A9, FUNCT_1:def 3;

        then

         A13: (F . a) <> a by A10, Th1;

         [(F . a), a] in (R |_2 Y) by A10, A12, Th1;

        then

         A14: [(F . a), a] in R by XBOOLE_0:def 4;

        ((R |_2 Y) -Seg a) c= Y by A9, Th9;

        then ( rng F) c= ( field R) by A1, A10;

        then [a, (F . a)] in R by A1, A2, A4, A9, A11, A7, Th35;

        hence contradiction by A13, A14, A2, Lm3;

      end;

      (R |_2 Y) is well-ordering by A2, Th25;

      hence thesis by A2, A3, Th52;

    end;

    theorem :: WELLORD1:54

    (R,S) are_isomorphic & R is well-ordering implies S is well-ordering by Th44;