wellset1.miz

    begin

    reserve a,b,x,y,z,z1,z2,z3,y1,y3,y4,A,B,C,D,G,M,N,X,Y,Z,W0,W00 for set,

R,S,T,W,W1,W2 for Relation,

F,H,H1 for Function;

    theorem :: WELLSET1:1



     Th1: for x be object holds x in ( field R) iff ex y be object st ( [x, y] in R or [y, x] in R)

    proof

      let x be object;

      x in (( dom R) \/ ( rng R)) iff x in ( dom R) or x in ( rng R) by XBOOLE_0:def 3;

      hence thesis by RELAT_1:def 6, XTUPLE_0:def 12, XTUPLE_0:def 13;

    end;

    theorem :: WELLSET1:2



     Th2: X <> {} & Y <> {} & W = [:X, Y:] implies ( field W) = (X \/ Y)

    proof

      set a = the Element of X, b = the Element of Y;

      assume that

       A1: X <> {} and

       A2: Y <> {} and

       A3: W = [:X, Y:];



       A4: for x be object holds x in ( field W) implies x in (X \/ Y)

      proof

        let x be object;

        assume x in ( field W);

        then

        consider y be object such that

         A5: [x, y] in W or [y, x] in W by Th1;



         A6: [y, x] in W implies x in (X \/ Y)

        proof

          assume [y, x] in W;

          then x in Y by A3, ZFMISC_1: 87;

          hence thesis by XBOOLE_0:def 3;

        end;

         [x, y] in W implies x in (X \/ Y)

        proof

          assume [x, y] in W;

          then x in X by A3, ZFMISC_1: 87;

          hence thesis by XBOOLE_0:def 3;

        end;

        hence thesis by A5, A6;

      end;

      for x be object holds x in (X \/ Y) implies x in ( field W)

      proof

        let x be object;



         A7: x in X implies x in ( field W)

        proof

          assume x in X;

          then [x, b] in W by A2, A3, ZFMISC_1: 87;

          hence thesis by Th1;

        end;



         A8: x in Y implies x in ( field W)

        proof

          assume x in Y;

          then [a, x] in W by A1, A3, ZFMISC_1: 87;

          hence thesis by Th1;

        end;

        assume x in (X \/ Y);

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

      end;

      hence thesis by A4, TARSKI: 2;

    end;

    scheme :: WELLSET1:sch1

    RSeparation { A() -> set , P[ Relation] } :

ex B st for R be Relation holds R in B iff R in A() & P[R];

      defpred p[ object, object] means $1 = $2 & ex S st S = $2 & P[S];



       A1: for y,t,v be object st p[y, t] & p[y, v] holds t = v;

      consider B such that

       A2: for t be object holds t in B iff ex y be object st y in A() & p[y, t] from TARSKI:sch 1( A1);

      take B;

      let R;

      R in B implies ex T st T in A() & T = R & P[R]

      proof

        assume R in B;

        then

        consider y be object such that

         A3: y in A() and

         A4: y = R and

         A5: ex S st S = R & P[S] by A2;

        reconsider y as Relation by A4;

        take y;

        thus thesis by A3, A4, A5;

      end;

      hence R in B implies R in A() & P[R];

      thus thesis by A2;

    end;

    theorem :: WELLSET1:3



     Th3: for x, y, W st x in ( field W) & y in ( field W) & W is well-ordering holds not x in (W -Seg y) implies [y, x] in W

    proof

      let x, y, W;

      assume that

       A1: x in ( field W) and

       A2: y in ( field W) and

       A3: W is well-ordering;

      W is connected by A3;

      then W is_connected_in ( field W) by RELAT_2:def 14;

      then

       A4: x <> y implies [x, y] in W or [y, x] in W by A1, A2, RELAT_2:def 6;

      W is reflexive by A3;

      then

       A5: W is_reflexive_in ( field W) by RELAT_2:def 9;

      assume not x in (W -Seg y);

      hence thesis by A1, A5, A4, RELAT_2:def 1, WELLORD1: 1;

    end;

    theorem :: WELLSET1:4



     Th4: for x, y, W st x in ( field W) & y in ( field W) & W is well-ordering holds x in (W -Seg y) implies not [y, x] in W

    proof

      let x, y, W;

      assume that

       A1: x in ( field W) & y in ( field W) and

       A2: W is well-ordering;

      W is antisymmetric by A2;

      then

       A3: W is_antisymmetric_in ( field W) by RELAT_2:def 12;

      assume x in (W -Seg y);

      then

       A4: x <> y & [x, y] in W by WELLORD1: 1;

      assume [y, x] in W;

      hence contradiction by A1, A3, A4, RELAT_2:def 4;

    end;

    theorem :: WELLSET1:5



     Th5: for F, D st (for X st X in D holds not (F . X) in X & (F . X) in ( union D)) holds ex R st ( field R) c= ( union D) & R is well-ordering & not ( field R) in D & for y st y in ( field R) holds (R -Seg y) in D & (F . (R -Seg y)) = y

    proof

      let F, D;

      assume

       A1: for X st X in D holds not (F . X) in X & (F . X) in ( union D);

      defpred P[ Relation] means $1 is well-ordering & for y st y in ( field $1) holds ($1 -Seg y) in D & (F . ($1 -Seg y)) = y;

      set W0 = ( bool [:( union D), ( union D):]);

      consider G such that

       A2: W in G iff W in W0 & P[W] from RSeparation;

      defpred P[ object, object] means ex W st [$1, $2] in W & W in G;

      consider S such that

       A3: for x,y be object holds [x, y] in S iff x in ( union D) & y in ( union D) & P[x, y] from RELAT_1:sch 1;

      take R = S;



       A4: x in ( field R) implies x in ( union D) & ex W st x in ( field W) & W in G

      proof

        assume x in ( field R);

        then

        consider y be object such that

         A5: [x, y] in R or [y, x] in R by Th1;

        (x in ( union D) & y in ( union D) & ex S st [x, y] in S & S in G) or (y in ( union D) & x in ( union D) & ex S st [y, x] in S & S in G) by A3, A5;

        then

        consider S such that

         A6: ( [x, y] in S or [y, x] in S) & S in G;

        thus x in ( union D) by A3, A5;

        take S;

        thus thesis by A6, Th1;

      end;

      then for x be object holds x in ( field R) implies x in ( union D);

      hence ( field R) c= ( union D);



       A7: for W1, W2 holds W1 in G & W2 in G implies ((W1 c= W2 & for x st x in ( field W1) holds (W1 -Seg x) = (W2 -Seg x)) or (W2 c= W1 & for x st x in ( field W2) holds (W2 -Seg x) = (W1 -Seg x)))

      proof

        let W1, W2;

        assume that

         A8: W1 in G and

         A9: W2 in G;



         A10: W2 is well-ordering by A2, A9;

        defpred P[ set] means $1 in ( field W2) & (W1 |_2 (W1 -Seg $1)) = (W2 |_2 (W2 -Seg $1));

        consider C such that

         A11: x in C iff x in ( field W1) & P[x] from XFAMILY:sch 1;



         A12: W1 is well-ordering by A2, A8;



         A13: x in C implies (W1 -Seg x) = (W2 -Seg x)

        proof

          assume

           A14: x in C;

          for y be object holds y in (W1 -Seg x) iff y in (W2 -Seg x)

          proof

            let y be object;

            ( field (W1 |_2 (W1 -Seg x))) = (W1 -Seg x) & ( field (W2 |_2 (W2 -Seg x))) = (W2 -Seg x) by A12, A10, WELLORD1: 32;

            hence thesis by A11, A14;

          end;

          hence thesis by TARSKI: 2;

        end;



         A15: x in C implies (W1 -Seg x) c= C

        proof

          assume

           A16: x in C;

          for y be object holds y in (W1 -Seg x) implies y in C

          proof

            let y be object;

            assume

             A17: y in (W1 -Seg x);

            then

             A18: y in (W2 -Seg x) by A13, A16;

            then

             A19: [y, x] in W2 by WELLORD1: 1;

            then

             A20: y in ( field W2) by RELAT_1: 15;



             A21: (W1 -Seg y) = ((W1 |_2 (W1 -Seg x)) -Seg y) by A12, A17, WELLORD1: 27

            .= ((W2 |_2 (W2 -Seg x)) -Seg y) by A11, A16

            .= (W2 -Seg y) by A10, A18, WELLORD1: 27;



             A22: [y, x] in W1 by A17, WELLORD1: 1;

            then

             A23: y in ( field W1) by RELAT_1: 15;

            x in ( field W2) by A19, RELAT_1: 15;

            then

             A24: (W2 -Seg y) c= (W2 -Seg x) by A10, A18, A20, WELLORD1: 30;

            x in ( field W1) by A22, RELAT_1: 15;

            then (W1 -Seg y) c= (W1 -Seg x) by A12, A17, A23, WELLORD1: 30;



            then (W1 |_2 (W1 -Seg y)) = ((W1 |_2 (W1 -Seg x)) |_2 (W1 -Seg y)) by WELLORD1: 22

            .= ((W2 |_2 (W2 -Seg x)) |_2 (W2 -Seg y)) by A11, A16, A21

            .= (W2 |_2 (W2 -Seg y)) by A24, WELLORD1: 22;

            hence thesis by A11, A23, A20;

          end;

          hence thesis;

        end;



         A25: for y1 be object holds y1 in ( field W1) & not y1 in C implies ex y3 st y3 in ( field W1) & C = (W1 -Seg y3) & not y3 in C

        proof

          let y1 be object;

          set Y = (( field W1) \ C);

          assume y1 in ( field W1) & not y1 in C;

          then Y <> {} by XBOOLE_0:def 5;

          then

          consider a be object such that

           A26: a in Y and

           A27: for b be object st b in Y holds [a, b] in W1 by A12, WELLORD1: 6;

          take y3 = a;

          for x be object holds x in C iff x in (W1 -Seg y3)

          proof

            let x be object;

            thus x in C implies x in (W1 -Seg y3)

            proof

              assume that

               A28: x in C and

               A29: not x in (W1 -Seg y3);

              x in ( field W1) by A11, A28;

              then

               A30: [y3, x] in W1 by A12, A26, A29, Th3;



               A31: (W1 -Seg x) c= C by A15, A28;

              y3 <> x implies y3 in C by A30, WELLORD1: 1, A31;

              hence contradiction by A26, A28, XBOOLE_0:def 5;

            end;

            thus x in (W1 -Seg y3) implies x in C

            proof

              assume that

               A32: x in (W1 -Seg y3) and

               A33: not x in C;

               [x, y3] in W1 by A32, WELLORD1: 1;

              then

               A34: x in ( field W1) by RELAT_1: 15;

              then x in Y by A33, XBOOLE_0:def 5;

              then [y3, x] in W1 by A27;

              hence contradiction by A12, A26, A32, A34, Th4;

            end;

          end;

          hence thesis by A26, TARSKI: 2, XBOOLE_0:def 5;

        end;



         A35: x in C implies (W2 -Seg x) c= C

        proof

          assume

           A36: x in C;

          let y be object;

          assume

           A37: y in (W2 -Seg x);

          then

           A38: y in (W1 -Seg x) by A13, A36;

          then

           A39: [y, x] in W1 by WELLORD1: 1;

          then

           A40: y in ( field W1) by RELAT_1: 15;



           A41: (W2 -Seg y) = ((W2 |_2 (W2 -Seg x)) -Seg y) by A10, A37, WELLORD1: 27

          .= ((W1 |_2 (W1 -Seg x)) -Seg y) by A11, A36

          .= (W1 -Seg y) by A12, A38, WELLORD1: 27;



           A42: [y, x] in W2 by A37, WELLORD1: 1;

          then

           A43: y in ( field W2) by RELAT_1: 15;

          x in ( field W1) by A39, RELAT_1: 15;

          then

           A44: (W1 -Seg y) c= (W1 -Seg x) by A12, A38, A40, WELLORD1: 30;

          x in ( field W2) by A42, RELAT_1: 15;

          then (W2 -Seg y) c= (W2 -Seg x) by A10, A37, A43, WELLORD1: 30;



          then (W2 |_2 (W2 -Seg y)) = ((W2 |_2 (W2 -Seg x)) |_2 (W2 -Seg y)) by WELLORD1: 22

          .= ((W1 |_2 (W1 -Seg x)) |_2 (W1 -Seg y)) by A11, A36, A41

          .= (W1 |_2 (W1 -Seg y)) by A44, WELLORD1: 22;

          hence thesis by A11, A43, A40;

        end;



         A45: y1 in ( field W2) & not y1 in C implies ex y3 st y3 in ( field W2) & C = (W2 -Seg y3) & not y3 in C

        proof

          set Y = (( field W2) \ C);

          assume y1 in ( field W2) & not y1 in C;

          then Y <> {} by XBOOLE_0:def 5;

          then

          consider a be object such that

           A46: a in Y and

           A47: for b be object st b in Y holds [a, b] in W2 by A10, WELLORD1: 6;

          take y3 = a;

          for x be object holds x in C iff x in (W2 -Seg y3)

          proof

            let x be object;

            thus x in C implies x in (W2 -Seg y3)

            proof

              assume that

               A48: x in C and

               A49: not x in (W2 -Seg y3);

              x in ( field W2) by A11, A48;

              then

               A50: [y3, x] in W2 by A10, A46, A49, Th3;



               A51: (W2 -Seg x) c= C by A35, A48;

              y3 <> x implies y3 in C by A50, WELLORD1: 1, A51;

              hence contradiction by A46, A48, XBOOLE_0:def 5;

            end;

            thus x in (W2 -Seg y3) implies x in C

            proof

              assume that

               A52: x in (W2 -Seg y3) and

               A53: not x in C;

               [x, y3] in W2 by A52, WELLORD1: 1;

              then

               A54: x in ( field W2) by RELAT_1: 15;

              then x in Y by A53, XBOOLE_0:def 5;

              then [y3, x] in W2 by A47;

              hence contradiction by A10, A46, A52, A54, Th4;

            end;

          end;

          hence thesis by A46, TARSKI: 2, XBOOLE_0:def 5;

        end;



         A55: C = ( field W1) or C = ( field W2)

        proof

          assume not C = ( field W1);

          then ex x be object st not (x in C implies x in ( field W1)) or not (x in ( field W1) implies x in C) by TARSKI: 2;

          then

          consider y3 such that

           A56: y3 in ( field W1) and

           A57: C = (W1 -Seg y3) and

           A58: not y3 in C by A11, A25;

          assume not C = ( field W2);

          then ex x be object st not (x in C implies x in ( field W2)) or not (x in ( field W2) implies x in C) by TARSKI: 2;

          then

          consider y4 such that

           A59: y4 in ( field W2) and

           A60: C = (W2 -Seg y4) and not y4 in C by A11, A45;



           A61: y3 = (F . (W2 -Seg y4)) by A2, A8, A56, A57, A60

          .= y4 by A2, A9, A59;

          for z be object holds z in (W1 |_2 (W1 -Seg y3)) iff z in (W2 |_2 (W2 -Seg y3))

          proof

            let z be object;



             A62: z in W1 & z in [:(W1 -Seg y3), (W1 -Seg y3):] implies z in W2 & z in [:(W2 -Seg y3), (W2 -Seg y3):]

            proof

              assume that

               A63: z in W1 and

               A64: z in [:(W1 -Seg y3), (W1 -Seg y3):];

              consider z1,z2 be object such that

               A65: z1 in (W1 -Seg y3) and

               A66: z2 in (W1 -Seg y3) and

               A67: z = [z1, z2] by A64, ZFMISC_1:def 2;

              z1 in (W1 -Seg z2) or z1 = z2 & not z1 in (W1 -Seg z2) by A63, A67, WELLORD1: 1;

              then

               A68: z1 in (W2 -Seg z2) or z1 = z2 & not z1 in (W2 -Seg z2) by A13, A57, A66;

              z1 in ( field W2) by A11, A57, A65;

              hence thesis by A10, A57, A60, A61, A64, A67, A68, Th3, WELLORD1: 1;

            end;

            z in W2 & z in [:(W2 -Seg y3), (W2 -Seg y3):] implies z in W1 & z in [:(W1 -Seg y3), (W1 -Seg y3):]

            proof

              assume that

               A69: z in W2 and

               A70: z in [:(W2 -Seg y3), (W2 -Seg y3):];

              consider z1,z2 be object such that

               A71: z1 in (W2 -Seg y3) and

               A72: z2 in (W2 -Seg y3) and

               A73: z = [z1, z2] by A70, ZFMISC_1:def 2;

              z1 in (W2 -Seg z2) or z1 = z2 & not z1 in (W2 -Seg z2) by A69, A73, WELLORD1: 1;

              then

               A74: z1 in (W1 -Seg z2) or z1 = z2 & not z1 in (W1 -Seg z2) by A13, A60, A61, A72;

              z1 in ( field W1) by A11, A60, A61, A71;

              hence thesis by A12, A57, A60, A61, A70, A73, A74, Th3, WELLORD1: 1;

            end;

            hence thesis by A62, XBOOLE_0:def 4;

          end;

          then (W1 |_2 (W1 -Seg y3)) = (W2 |_2 (W2 -Seg y3)) by TARSKI: 2;

          hence contradiction by A11, A56, A58, A59, A61;

        end;



         A75: C = ( field W2) implies (W2 c= W1 & for x st x in ( field W2) holds (W2 -Seg x) = (W1 -Seg x))

        proof

          assume

           A76: C = ( field W2);

          for z1,z2 be object holds [z1, z2] in W2 implies [z1, z2] in W1

          proof

            let z1,z2 be object;

            assume

             A77: [z1, z2] in W2;

            then

             A78: z1 in (W2 -Seg z2) or z1 = z2 & not z1 in (W2 -Seg z2) by WELLORD1: 1;

            z1 in C by A76, A77, RELAT_1: 15;

            then

             A79: z1 in ( field W1) by A11;

            z2 in C by A76, A77, RELAT_1: 15;

            then z1 in (W1 -Seg z2) or z1 = z2 & not z1 in (W1 -Seg z2) by A13, A78;

            hence thesis by A12, A79, Th3, WELLORD1: 1;

          end;

          hence thesis by A13, A76, RELAT_1:def 3;

        end;

        C = ( field W1) implies (W1 c= W2 & for x st x in ( field W1) holds (W1 -Seg x) = (W2 -Seg x))

        proof

          assume

           A80: C = ( field W1);

          for z1,z2 be object holds [z1, z2] in W1 implies [z1, z2] in W2

          proof

            let z1,z2 be object;

            assume

             A81: [z1, z2] in W1;

            then

             A82: z1 in (W1 -Seg z2) or z1 = z2 & not z1 in (W1 -Seg z2) by WELLORD1: 1;

            z1 in C by A80, A81, RELAT_1: 15;

            then

             A83: z1 in ( field W2) by A11;

            z2 in C by A80, A81, RELAT_1: 15;

            then z1 in (W2 -Seg z2) or z1 = z2 & not z1 in (W2 -Seg z2) by A13, A82;

            hence thesis by A10, A83, Th3, WELLORD1: 1;

          end;

          hence thesis by A13, A80, RELAT_1:def 3;

        end;

        hence thesis by A55, A75;

      end;



       A84: for x,y be object holds x in ( field R) & y in ( field R) & [x, y] in R & [y, x] in R implies x = y

      proof

        let x,y be object;

        assume that x in ( field R) and y in ( field R) and

         A85: [x, y] in R and

         A86: [y, x] in R;

        consider W1 such that

         A87: [x, y] in W1 and

         A88: W1 in G by A3, A85;

        consider W2 such that

         A89: [y, x] in W2 and

         A90: W2 in G by A3, A86;



         A91: W2 c= W1 implies x = y

        proof

          W1 is well-ordering by A2, A88;

          then W1 well_orders ( field W1) by WELLORD1: 4;

          then

           A92: W1 is_antisymmetric_in ( field W1);

          assume

           A93: W2 c= W1;

          then x in ( field W1) & y in ( field W1) by A89, RELAT_1: 15;

          hence thesis by A87, A89, A93, A92, RELAT_2:def 4;

        end;

        W1 c= W2 implies x = y

        proof

          W2 is well-ordering by A2, A90;

          then W2 well_orders ( field W2) by WELLORD1: 4;

          then

           A94: W2 is_antisymmetric_in ( field W2);

          assume

           A95: W1 c= W2;

          then x in ( field W2) & y in ( field W2) by A87, RELAT_1: 15;

          hence thesis by A87, A89, A95, A94, RELAT_2:def 4;

        end;

        hence thesis by A7, A88, A90, A91;

      end;

      then

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



       A97: W in G implies ( field W) c= ( field R)

      proof

        assume

         A98: W in G;

        let x be object;

        assume x in ( field W);

        then

        consider y be object such that

         A99: [x, y] in W or [y, x] in W by Th1;



         A100: [y, x] in W implies [y, x] in R

        proof

          assume

           A101: [y, x] in W;

          W in W0 by A2, A98;

          then ex z1,z2 be object st z1 in ( union D) & z2 in ( union D) & [y, x] = [z1, z2] by A101, ZFMISC_1: 84;

          hence thesis by A3, A98, A101;

        end;

         [x, y] in W implies [x, y] in R

        proof

          assume

           A102: [x, y] in W;

          W in W0 by A2, A98;

          then ex z1,z2 be object st z1 in ( union D) & z2 in ( union D) & [x, y] = [z1, z2] by A102, ZFMISC_1: 84;

          hence thesis by A3, A98, A102;

        end;

        hence thesis by A99, A100, Th1;

      end;



       A103: for y st y in ( field R) holds (R -Seg y) in D & (F . (R -Seg y)) = y

      proof

        let y;

        assume

         A104: y in ( field R);

        then

        consider W such that

         A105: y in ( field W) and

         A106: W in G by A4;



         A107: y in ( union D) by A4, A104;



         A108: ( field W) c= ( field R) by A97, A106;



         A109: for x be object holds x in (W -Seg y) implies x in (R -Seg y)

        proof

          let x be object;

          assume

           A110: x in (W -Seg y);

          then

           A111: [x, y] in W by WELLORD1: 1;

          then x in ( field W) by RELAT_1: 15;

          then x in ( union D) by A4, A108;

          then

           A112: [x, y] in R by A3, A106, A107, A111;

           not x = y by A110, WELLORD1: 1;

          hence thesis by A112, WELLORD1: 1;

        end;

        for x be object holds x in (R -Seg y) implies x in (W -Seg y)

        proof

          let x be object;

          assume

           A113: x in (R -Seg y);

          then [x, y] in R by WELLORD1: 1;

          then

          consider W1 such that

           A114: [x, y] in W1 and

           A115: W1 in G by A3;



           A116: y in ( field W1) by A114, RELAT_1: 15;

           not x = y by A113, WELLORD1: 1;

          then x in (W1 -Seg y) by A114, WELLORD1: 1;

          hence thesis by A7, A105, A106, A115, A116;

        end;

        then (W -Seg y) = (R -Seg y) by A109, TARSKI: 2;

        hence thesis by A2, A105, A106;

      end;



       A117: 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

      proof

        let x,y be object;

        assume that

         A118: x in ( field R) and

         A119: y in ( field R) and

         A120: x <> y;

        consider W2 such that

         A121: y in ( field W2) and

         A122: W2 in G by A4, A119;

        consider W1 such that

         A123: x in ( field W1) and

         A124: W1 in G by A4, A118;



         A125: x in ( union D) & y in ( union D) by A4, A118, A119;



         A126: W2 c= W1 implies [x, y] in R or [y, x] in R

        proof

          W1 is well-ordering by A2, A124;

          then W1 well_orders ( field W1) by WELLORD1: 4;

          then

           A127: W1 is_connected_in ( field W1);

          assume W2 c= W1;

          then ( field W2) c= ( field W1) by RELAT_1: 16;

          then [x, y] in W1 or [y, x] in W1 by A120, A123, A121, A127, RELAT_2:def 6;

          hence thesis by A3, A124, A125;

        end;

        W1 c= W2 implies [x, y] in R or [y, x] in R

        proof

          W2 is well-ordering by A2, A122;

          then W2 well_orders ( field W2) by WELLORD1: 4;

          then

           A128: W2 is_connected_in ( field W2);

          assume W1 c= W2;

          then ( field W1) c= ( field W2) by RELAT_1: 16;

          then [x, y] in W2 or [y, x] in W2 by A120, A123, A121, A128, RELAT_2:def 6;

          hence thesis by A3, A125, A122;

        end;

        hence thesis by A7, A124, A122, A126;

      end;

      then

       A129: R is_connected_in ( field R) by RELAT_2:def 6;



       A130: R is_well_founded_in ( field R)

      proof

        let Y;

        assume that

         A131: Y c= ( field R) and

         A132: Y <> {} ;

        set y = the Element of Y;

        y in ( field R) by A131, A132;

        then

        consider W such that

         A133: y in ( field W) and

         A134: W in G by A4;

        W is well-ordering by A2, A134;

        then W well_orders ( field W) by WELLORD1: 4;

        then

         A135: W is_well_founded_in ( field W);

        set A = (Y /\ ( field W));



         A136: A c= ( field W) by XBOOLE_1: 17;

        A <> {} by A132, A133, XBOOLE_0:def 4;

        then

        consider a be object such that

         A137: a in A and

         A138: (W -Seg a) misses A by A135, A136;

        ex b be object st b in Y & (R -Seg b) misses Y

        proof

          take b = a;

          thus b in Y by A137, XBOOLE_0:def 4;

          assume not thesis;

          then

          consider x be object such that

           A139: x in (R -Seg b) and

           A140: x in Y by XBOOLE_0: 3;

           [x, b] in R by A139, WELLORD1: 1;

          then

          consider W1 such that

           A141: [x, b] in W1 and

           A142: W1 in G by A3;



           A143: b in ( field W1) by A141, RELAT_1: 15;

          x <> b by A139, WELLORD1: 1;

          then x in (W1 -Seg b) by A141, WELLORD1: 1;

          then

           A144: x in (W -Seg a) by A7, A134, A136, A137, A142, A143;

          then [x, a] in W by WELLORD1: 1;

          then x in ( field W) by RELAT_1: 15;

          then x in A by A140, XBOOLE_0:def 4;

          hence contradiction by A138, A144, XBOOLE_0: 3;

        end;

        hence thesis;

      end;



       A145: for x,y,z be object holds x in ( field R) & y in ( field R) & z in ( field R) & [x, y] in R & [y, z] in R implies [x, z] in R

      proof

        let x,y,z be object;

        assume that x in ( field R) and y in ( field R) and z in ( field R) and

         A146: [x, y] in R and

         A147: [y, z] in R;



         A148: x in ( union D) & z in ( union D) by A3, A146, A147;

        consider W1 such that

         A149: [x, y] in W1 and

         A150: W1 in G by A3, A146;

        consider W2 such that

         A151: [y, z] in W2 and

         A152: W2 in G by A3, A147;

        ex W st [x, y] in W & [y, z] in W & W in G

        proof

          take W = W2;



           A153: not x in (W1 -Seg y) implies [x, y] in W

          proof



             A154: W1 is well-ordering by A2, A150;

            then W1 well_orders ( field W1) by WELLORD1: 4;

            then

             A155: W1 is_antisymmetric_in ( field W1);

            W is well-ordering by A2, A152;

            then W well_orders ( field W) by WELLORD1: 4;

            then

             A156: W is_reflexive_in ( field W);



             A157: x in ( field W1) & y in ( field W1) by A149, RELAT_1: 15;

            assume not x in (W1 -Seg y);

            then [y, x] in W1 by A157, A154, Th3;

            then

             A158: x = y by A149, A157, A155, RELAT_2:def 4;

            y in ( field W) by A151, RELAT_1: 15;

            hence thesis by A158, A156, RELAT_2:def 1;

          end;

          y in ( field W1) & y in ( field W) by A149, A151, RELAT_1: 15;

          then (W1 -Seg y) = (W -Seg y) by A7, A150, A152;

          hence thesis by A151, A152, A153, WELLORD1: 1;

        end;

        then

        consider W such that

         A159: [x, y] in W and

         A160: [y, z] in W and

         A161: W in G;



         A162: z in ( field W) by A160, RELAT_1: 15;

        W is well-ordering by A2, A161;

        then W well_orders ( field W) by WELLORD1: 4;

        then

         A163: W is_transitive_in ( field W);

        x in ( field W) & y in ( field W) by A159, RELAT_1: 15;

        then [x, z] in W by A159, A160, A163, A162, RELAT_2:def 8;

        hence thesis by A3, A148, A161;

      end;

      then

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



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

      proof

        let x be object;

        assume

         A166: x in ( field R);

        then

        consider W such that

         A167: x in ( field W) and

         A168: W in G by A4;

        W is well-ordering by A2, A168;

        then W well_orders ( field W) by WELLORD1: 4;

        then W is_reflexive_in ( field W);

        then

         A169: [x, x] in W by A167, RELAT_2:def 1;

        x in ( union D) by A4, A166;

        hence thesis by A3, A168, A169;

      end;



       A170: not ( field R) in D

      proof

        set a0 = (F . ( field R));

        reconsider W3 = [:( field R), {a0}:] as Relation;

        reconsider W4 = { [a0, a0]} as Relation;

        reconsider W1 = ((R \/ [:( field R), {a0}:]) \/ { [a0, a0]}) as Relation;

         { [a0, a0]} c= W1 & [a0, a0] in { [a0, a0]} by TARSKI:def 1, XBOOLE_1: 7;

        then

         A171: a0 in ( field W1) by RELAT_1: 15;

        ( field W4) = {a0, a0} by RELAT_1: 17;

        then

         A172: ( field W4) = ( {a0} \/ {a0}) by ENUMSET1: 1;



         A173: ( field R) = {} implies ( field W1) = (( field R) \/ {a0})

        proof

          assume

           A174: ( field R) = {} ;



           A175: ( field W3) = {}

          proof

            set z3 = the Element of ( field W3);

            assume ( field W3) <> {} ;

            then ex z2 be object st [z3, z2] in W3 or [z2, z3] in W3 by Th1;

            hence contradiction by A174, ZFMISC_1: 90;

          end;

          ( field W1) = (( field (R \/ W3)) \/ ( field W4)) by RELAT_1: 18;

          then ( field W1) = ((( field R) \/ {} ) \/ {a0}) by A172, A175, RELAT_1: 18;

          hence thesis;

        end;



         A176: ( field R) <> {} implies ( field W1) = (( field R) \/ {a0})

        proof

          assume ( field R) <> {} ;

          then

           A177: ( field W3) = (( field R) \/ {a0}) by Th2;

          ( field W1) = (( field (R \/ W3)) \/ ( field W4)) by RELAT_1: 18;

          then ( field W1) = ((( field R) \/ (( field R) \/ {a0})) \/ {a0}) by A172, A177, RELAT_1: 18;

          then ( field W1) = (((( field R) \/ ( field R)) \/ {a0}) \/ {a0}) by XBOOLE_1: 4;

          then ( field W1) = ((( field R) \/ ( field R)) \/ ( {a0} \/ {a0})) by XBOOLE_1: 4;

          hence thesis;

        end;



         A178: x in ( field W1) implies x in ( field R) or x = a0

        proof

          assume x in ( field W1);

          then x in ( field R) or x in {a0} by A176, A173, XBOOLE_0:def 3;

          hence thesis by TARSKI:def 1;

        end;



         A179: for x,y be object holds [x, y] in W1 iff [x, y] in R or [x, y] in W3 or [x, y] in W4

        proof

          let x,y be object;

           [x, y] in W1 iff ( [x, y] in (R \/ W3) or [x, y] in W4) by XBOOLE_0:def 3;

          hence thesis by XBOOLE_0:def 3;

        end;

        for x,y be object holds x in ( field W1) & y in ( field W1) & x <> y implies [x, y] in W1 or [y, x] in W1

        proof

          let x,y be object;

          assume that

           A180: x in ( field W1) and

           A181: y in ( field W1) and

           A182: x <> y;



           A183: not x in ( field R) implies [x, y] in W1 or [y, x] in W1

          proof

            assume not x in ( field R);

            then

             A184: x = a0 by A178, A180;



             A185: y in ( field R) implies [x, y] in W1 or [y, x] in W1

            proof

              assume y in ( field R);

              then [y, x] in W3 by A184, ZFMISC_1: 106;

              hence thesis by A179;

            end;

            y = a0 implies [x, y] in W1 or [y, x] in W1

            proof

              assume y = a0;

              then [x, y] in W4 by A184, TARSKI:def 1;

              hence thesis by A179;

            end;

            hence thesis by A178, A181, A185;

          end;



           A186: not y in ( field R) implies [x, y] in W1 or [y, x] in W1

          proof

            assume not y in ( field R);

            then

             A187: y = a0 by A178, A181;



             A188: x in ( field R) implies [y, x] in W1 or [x, y] in W1

            proof

              assume x in ( field R);

              then [x, y] in W3 by A187, ZFMISC_1: 106;

              hence thesis by A179;

            end;

            x = a0 implies [y, x] in W1 or [x, y] in W1

            proof

              assume x = a0;

              then [y, x] in W4 by A187, TARSKI:def 1;

              hence thesis by A179;

            end;

            hence thesis by A178, A180, A188;

          end;

          x in ( field R) & y in ( field R) implies [x, y] in W1 or [y, x] in W1

          proof

            assume x in ( field R) & y in ( field R);

            then [x, y] in R or [y, x] in R by A117, A182;

            hence thesis by A179;

          end;

          hence thesis by A183, A186;

        end;

        then

         A189: W1 is_connected_in ( field W1) by RELAT_2:def 6;

        assume

         A190: ( field R) in D;

        for x,y be object holds [x, y] in W1 implies [x, y] in [:( union D), ( union D):]

        proof

          let x,y be object;

          assume

           A191: [x, y] in W1;

          then y in ( field W1) by RELAT_1: 15;

          then y in ( field R) or y = a0 by A178;

          then

           A192: y in ( union D) by A1, A4, A190;

          x in ( field W1) by A191, RELAT_1: 15;

          then x in ( field R) or x = a0 by A178;

          then x in ( union D) by A1, A4, A190;

          hence thesis by A192, ZFMISC_1:def 2;

        end;

        then

         A193: W1 c= [:( union D), ( union D):] by RELAT_1:def 3;



         A194: not a0 in ( field R) by A1, A190;



         A195: for x,y be object holds [x, y] in W1 & y in ( field R) implies [x, y] in R & x in ( field R)

        proof

          let x,y be object;

          assume that

           A196: [x, y] in W1 and

           A197: y in ( field R);



           A198: not [x, y] in W4

          proof

            assume [x, y] in W4;

            then [x, y] = [a0, a0] by TARSKI:def 1;

            hence contradiction by A194, A197, XTUPLE_0: 1;

          end;

           not [x, y] in W3 by A194, A197, ZFMISC_1: 106;

          hence [x, y] in R by A179, A196, A198;

           [x, y] in R or [x, y] in W3 or [x, y] in W4 by A179, A196;

          hence thesis by A198, RELAT_1: 15, ZFMISC_1: 106;

        end;

        for x,y be object holds x in ( field W1) & y in ( field W1) & [x, y] in W1 & [y, x] in W1 implies x = y

        proof

          let x,y be object;

          assume that

           A199: x in ( field W1) and

           A200: y in ( field W1) and

           A201: [x, y] in W1 and

           A202: [y, x] in W1;



           A203: x in ( field R) implies x = y

          proof

            assume

             A204: x in ( field R);

            then

             A205: [y, x] in R by A195, A202;



             A206: y in ( field R) by A195, A202, A204;

            then [x, y] in R by A195, A201;

            hence thesis by A84, A204, A205, A206;

          end;



           A207: y in ( field R) implies x = y

          proof

            assume

             A208: y in ( field R);

            then

             A209: [x, y] in R by A195, A201;



             A210: x in ( field R) by A195, A201, A208;

            then [y, x] in R by A195, A202;

            hence thesis by A84, A208, A209, A210;

          end;

          y in ( field R) or y = a0 by A178, A200;

          hence thesis by A178, A199, A203, A207;

        end;

        then

         A211: W1 is_antisymmetric_in ( field W1) by RELAT_2:def 4;



         A212: y in ( field R) implies (W1 -Seg y) = (R -Seg y)

        proof

          assume

           A213: y in ( field R);



           A214: for x be object holds x in (W1 -Seg y) implies x in (R -Seg y)

          proof

            let x be object;

            assume

             A215: x in (W1 -Seg y);

            then [x, y] in W1 by WELLORD1: 1;

            then

             A216: [x, y] in R by A195, A213;

            x <> y by A215, WELLORD1: 1;

            hence thesis by A216, WELLORD1: 1;

          end;

          for x be object holds x in (R -Seg y) implies x in (W1 -Seg y)

          proof

            let x be object;

            assume

             A217: x in (R -Seg y);

            then [x, y] in R by WELLORD1: 1;

            then

             A218: [x, y] in W1 by A179;

            x <> y by A217, WELLORD1: 1;

            hence thesis by A218, WELLORD1: 1;

          end;

          hence thesis by A214, TARSKI: 2;

        end;



         A219: W1 is_well_founded_in ( field W1)

        proof

          let Y;

          assume that

           A220: Y c= ( field W1) and

           A221: Y <> {} ;



           A222: not Y c= ( field R) implies ex a st a in Y & (W1 -Seg a) misses Y

          proof

            assume not Y c= ( field R);



             A223: not (( field R) /\ Y) = {} implies ex a st a in Y & (W1 -Seg a) misses Y

            proof

              set X = (( field R) /\ Y);



               A224: X c= ( field R) by XBOOLE_1: 17;

              assume not (( field R) /\ Y) = {} ;

              then

              consider y be object such that

               A225: y in X and

               A226: (R -Seg y) misses X by A130, A224;



               A227: ((R -Seg y) /\ Y) c= ((R -Seg y) /\ X)

              proof

                let x be object;

                assume

                 A228: x in ((R -Seg y) /\ Y);

                then

                 A229: x in Y by XBOOLE_0:def 4;



                 A230: x in (R -Seg y) by A228, XBOOLE_0:def 4;

                then [x, y] in R by WELLORD1: 1;

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

                then x in X by A229, XBOOLE_0:def 4;

                hence thesis by A230, XBOOLE_0:def 4;

              end;

              ((R -Seg y) /\ X) = {} by A226, XBOOLE_0:def 7;

              then ((W1 -Seg y) /\ Y) = {} by A212, A224, A225, A227;

              then

               A231: (W1 -Seg y) misses Y by XBOOLE_0:def 7;

              y in Y by A225, XBOOLE_0:def 4;

              hence thesis by A231;

            end;

            (( field R) /\ Y) = {} implies ex a st a in Y & (W1 -Seg a) misses Y

            proof

              set y = the Element of Y;



               A232: (W1 -Seg a0) c= ( field R)

              proof

                let z be object;

                assume

                 A233: z in (W1 -Seg a0);

                then [z, a0] in W1 by WELLORD1: 1;

                then

                 A234: z in ( field W1) by RELAT_1: 15;

                z <> a0 by A233, WELLORD1: 1;

                hence thesis by A178, A234;

              end;



               A235: y in ( field W1) by A220, A221;

              assume

               A236: (( field R) /\ Y) = {} ;

              then not y in ( field R) by A221, XBOOLE_0:def 4;

              then y = a0 by A178, A235;

              then ((W1 -Seg y) /\ Y) = {} by A236, A232, XBOOLE_1: 3, XBOOLE_1: 26;

              then (W1 -Seg y) misses Y by XBOOLE_0:def 7;

              hence thesis by A221;

            end;

            hence thesis by A223;

          end;

          Y c= ( field R) implies ex a st a in Y & (W1 -Seg a) misses Y

          proof

            assume

             A237: Y c= ( field R);

            then

            consider b be object such that

             A238: b in Y & (R -Seg b) misses Y by A130, A221;

            take b;

            thus thesis by A212, A237, A238;

          end;

          hence thesis by A222;

        end;



         A239: for y st y in ( field W1) holds (W1 -Seg y) in D & (F . (W1 -Seg y)) = y

        proof

          let y;



           A240: y in ( field R) implies (W1 -Seg y) = (R -Seg y)

          proof

            assume

             A241: y in ( field R);



             A242: for x be object holds x in (W1 -Seg y) implies x in (R -Seg y)

            proof

              let x be object;



               A243: [x, y] in W4 implies [x, y] = [a0, a0] by TARSKI:def 1;

              assume

               A244: x in (W1 -Seg y);

              then [x, y] in W1 by WELLORD1: 1;

              then [x, y] in (R \/ W3) or [x, y] in W4 by XBOOLE_0:def 3;

              then

               A245: [x, y] in R or [x, y] in W3 or [x, y] in W4 by XBOOLE_0:def 3;

               not x = y by A244, WELLORD1: 1;

              hence thesis by A194, A241, A245, A243, WELLORD1: 1, XTUPLE_0: 1, ZFMISC_1: 106;

            end;

            for x be object holds x in (R -Seg y) implies x in (W1 -Seg y)

            proof

              let x be object;

              assume

               A246: x in (R -Seg y);

              then [x, y] in R by WELLORD1: 1;

              then [x, y] in (R \/ W3) by XBOOLE_0:def 3;

              then

               A247: [x, y] in W1 by XBOOLE_0:def 3;

               not x = y by A246, WELLORD1: 1;

              hence thesis by A247, WELLORD1: 1;

            end;

            hence thesis by A242, TARSKI: 2;

          end;



           A248: for x be object holds x in (W1 -Seg a0) implies x in ( field R)

          proof

            let x be object;

            assume

             A249: x in (W1 -Seg a0);

            then [x, a0] in W1 by WELLORD1: 1;

            then

             A250: x in ( field W1) by RELAT_1: 15;

             not x = a0 by A249, WELLORD1: 1;

            hence thesis by A178, A250;

          end;



           A251: for x be object holds x in ( field R) implies x in (W1 -Seg a0)

          proof

            let x be object;

            assume

             A252: x in ( field R);

            then [x, a0] in W3 by ZFMISC_1: 106;

            then [x, a0] in (R \/ W3) by XBOOLE_0:def 3;

            then [x, a0] in W1 by XBOOLE_0:def 3;

            hence thesis by A194, A252, WELLORD1: 1;

          end;

          assume y in ( field W1);

          then y in ( field R) or y = a0 by A178;

          hence thesis by A103, A190, A240, A248, A251, TARSKI: 2;

        end;

        for x,y,z be object holds x in ( field W1) & y in ( field W1) & z in ( field W1) & [x, y] in W1 & [y, z] in W1 implies [x, z] in W1

        proof

          let x,y,z be object;

          assume that

           A253: x in ( field W1) and y in ( field W1) and

           A254: z in ( field W1) and

           A255: [x, y] in W1 and

           A256: [y, z] in W1;



           A257: z = a0 implies [x, z] in W1

          proof

            assume

             A258: z = a0;



             A259: x = a0 implies [x, z] in W1

            proof

              assume x = a0;

              then [x, z] in W4 by A258, TARSKI:def 1;

              hence thesis by A179;

            end;

            x in ( field R) implies [x, z] in W1

            proof

              assume x in ( field R);

              then [x, z] in W3 by A258, ZFMISC_1: 106;

              hence thesis by A179;

            end;

            hence thesis by A178, A253, A259;

          end;

          z in ( field R) implies [x, z] in W1

          proof

            assume

             A260: z in ( field R);

            then

             A261: [y, z] in R by A195, A256;



             A262: y in ( field R) by A195, A256, A260;

            then [x, y] in R & x in ( field R) by A195, A255;

            then [x, z] in R by A145, A260, A261, A262;

            hence thesis by A179;

          end;

          hence thesis by A178, A254, A257;

        end;

        then

         A263: W1 is_transitive_in ( field W1) by RELAT_2:def 8;

        for x be object holds x in ( field W1) implies [x, x] in W1

        proof

          let x be object;



           A264: x = a0 implies [x, x] in W1

          proof



             A265: [a0, a0] in W4 by TARSKI:def 1;

            assume x = a0;

            hence thesis by A179, A265;

          end;



           A266: x in ( field R) implies [x, x] in W1 by A165, A179;

          assume x in ( field W1);

          hence thesis by A178, A266, A264;

        end;

        then W1 is_reflexive_in ( field W1) by RELAT_2:def 1;

        then W1 well_orders ( field W1) by A263, A211, A189, A219;

        then W1 is well-ordering by WELLORD1: 4;

        then W1 in G by A2, A193, A239;

        then ( field W1) c= ( field R) by A97;

        hence contradiction by A1, A190, A171;

      end;

      R is_reflexive_in ( field R) by A165, RELAT_2:def 1;

      then R well_orders ( field R) by A164, A96, A129, A130;

      hence thesis by A103, A170, WELLORD1: 4;

    end;

    theorem :: WELLSET1:6

    for N holds ex R st R is well-ordering & ( field R) = N

    proof

      let N;

      consider M such that

       A1: N in M & for X, Y holds X in M & Y c= X implies Y in M and

       A2: for X holds X in M implies ( bool X) in M and

       A3: for X holds X c= M implies (X,M) are_equipotent or X in M by ZFMISC_1: 112;

      defpred P[ set] means not ($1,M) are_equipotent ;

      consider D such that

       A4: A in D iff A in ( bool M) & P[A] from XFAMILY:sch 1;



       A5: ( union D) c= M

      proof

        let x be object;

        assume x in ( union D);

        then

        consider A such that

         A6: x in A and

         A7: A in D by TARSKI:def 4;

        A in ( bool M) by A4, A7;

        hence thesis by A6;

      end;

      set F = ( id D);

      for Z st Z in D holds not (F . Z) in Z & (F . Z) in ( union D)

      proof

        let Z;

        assume

         A8: Z in D;

         not Z in Z;

        hence not (F . Z) in Z by A8, FUNCT_1: 18;

        X in D implies X in ( union D)

        proof



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

          assume X in D;

          then

           A10: X in ( bool M) & not (X,M) are_equipotent by A4;



           A11: not ( {X},M) are_equipotent

          proof



             A12: X <> ( bool X)

            proof

              assume X = ( bool X);

              then not X in ( bool X);

              hence contradiction by ZFMISC_1:def 1;

            end;

            assume ( {X},M) are_equipotent ;

            then

            consider Z such that for x be object st x in {X} holds ex y be object st y in M & [x, y] in Z and

             A13: for y be object st y in M holds ex x be object st x in {X} & [x, y] in Z and

             A14: for x,z1,y,z2 be object st [x, z1] in Z & [y, z2] in Z holds x = y iff z1 = z2;

            ( bool X) in M by A2, A3, A10;

            then

            consider y be object such that

             A15: y in {X} and

             A16: [y, ( bool X)] in Z by A13;

            consider x be object such that

             A17: x in {X} and

             A18: [x, X] in Z by A3, A10, A13;

            x = X by A17, TARSKI:def 1;

            then y = x by A15, TARSKI:def 1;

            hence contradiction by A14, A12, A18, A16;

          end;

          X in M by A3, A10;

          then for x be object holds x in {X} implies x in M by TARSKI:def 1;

          then {X} c= M;

          then {X} in D by A4, A11;

          hence thesis by A9, TARSKI:def 4;

        end;

        then Z in ( union D) by A8;

        hence thesis by A8, FUNCT_1: 18;

      end;

      then

      consider S such that

       A19: ( field S) c= ( union D) and

       A20: S is well-ordering and

       A21: not ( field S) in D and for y st y in ( field S) holds (S -Seg y) in D & (F . (S -Seg y)) = y by Th5;

       not ( field S) c= M or (( field S),M) are_equipotent by A4, A21;

      then

      consider Z such that

       A22: for x be object st x in ( field S) holds ex y be object st y in M & [x, y] in Z and

       A23: for y be object st y in M holds ex x be object st x in ( field S) & [x, y] in Z and

       A24: for x,z1,y,z2 be object st [x, z1] in Z & [y, z2] in Z holds x = y iff z1 = z2 by A5, A19;

      defpred Q[ object, object] means [$2, $1] in Z;



       A25: for x be object st x in M holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in M;

        then ex y be object st y in ( field S) & [y, x] in Z by A23;

        hence thesis;

      end;



       A26: for x,z1,z2 be object st x in M & Q[x, z1] & Q[x, z2] holds z1 = z2 by A24;

      consider H such that

       A27: ( dom H) = M and

       A28: for x be object st x in M holds Q[x, (H . x)] from FUNCT_1:sch 2( A26, A25);

      defpred R[ object, object] means $2 = {$1};

      defpred P[ object] means ex x,y be object st $1 = [x, y] & [(H . x), (H . y)] in S;

      consider W0 such that

       A29: for z be object holds z in W0 iff z in [:M, M:] & P[z] from XBOOLE_0:sch 1;



       A30: for x be object holds x in ( field S) implies x in ( rng H)

      proof

        let x be object;

        assume x in ( field S);

        then

        consider y be object such that

         A31: y in M and

         A32: [x, y] in Z by A22;

        set z1 = (H . y);

        z1 in ( rng H) & [z1, y] in Z by A27, A28, A31, FUNCT_1:def 3;

        hence thesis by A24, A32;

      end;

      for z1,z2 be object st z1 in ( dom H) & z2 in ( dom H) & (H . z1) = (H . z2) holds z1 = z2

      proof

        let z1,z2 be object;

        assume that

         A33: z1 in ( dom H) & z2 in ( dom H) and

         A34: (H . z1) = (H . z2);

         [(H . z1), z1] in Z & [(H . z2), z2] in Z by A27, A28, A33;

        hence thesis by A24, A34;

      end;

      then

       A35: H is one-to-one by FUNCT_1:def 4;

      for z be object st z in W0 holds ex x,y be object st z = [x, y]

      proof

        let z be object;

        assume z in W0;

        then ex z1,z2 be object st z = [z1, z2] & [(H . z1), (H . z2)] in S by A29;

        hence thesis;

      end;

      then

      reconsider W0 as Relation by RELAT_1:def 1;



       A36: for z be object holds z in ( field W0) implies z in M

      proof

        let z be object;

        assume z in ( field W0);

        then

        consider z1 be object such that

         A37: [z, z1] in W0 or [z1, z] in W0 by Th1;



         A38: [z1, z] in W0 implies z in M

        proof

          assume [z1, z] in W0;

          then [z1, z] in [:M, M:] by A29;

          hence thesis by ZFMISC_1: 87;

        end;

         [z, z1] in W0 implies z in M

        proof

          assume [z, z1] in W0;

          then [z, z1] in [:M, M:] by A29;

          hence thesis by ZFMISC_1: 87;

        end;

        hence thesis by A37, A38;

      end;



       A39: for x be object st x in N holds ex y be object st R[x, y];



       A40: for x,z1,z2 be object st x in N & R[x, z1] & R[x, z2] holds z1 = z2;

      consider H1 such that

       A41: ( dom H1) = N and

       A42: for x be object st x in N holds R[x, (H1 . x)] from FUNCT_1:sch 2( A40, A39);

      for z1,z2 be object st z1 in ( dom H1) & z2 in ( dom H1) & (H1 . z1) = (H1 . z2) holds z1 = z2

      proof

        let z1,z2 be object;

        assume that

         A43: z1 in ( dom H1) and

         A44: z2 in ( dom H1) and

         A45: (H1 . z1) = (H1 . z2);

        (H1 . z1) = {z1} by A41, A42, A43;

        then

         A46: z1 in (H1 . z2) by A45, TARSKI:def 1;

        (H1 . z2) = {z2} by A41, A42, A44;

        hence thesis by A46, TARSKI:def 1;

      end;

      then

       A47: H1 is one-to-one by FUNCT_1:def 4;

      set S1 = (W0 |_2 ( rng H1));

      for x be object holds x in ( rng H) implies x in ( field S)

      proof

        let x be object;

        assume x in ( rng H);

        then

        consider z1 be object such that

         A48: z1 in ( dom H) & x = (H . z1) by FUNCT_1:def 3;

        (ex z2 be object st z2 in ( field S) & [z2, z1] in Z) & [x, z1] in Z by A23, A27, A28, A48;

        hence thesis by A24;

      end;

      then

       A49: ( rng H) = ( field S) by A30, TARSKI: 2;

      for z be object holds z in M implies z in ( field W0)

      proof

        let z be object;

        assume

         A50: z in M;

        ex z1 be object st [z, z1] in W0 or [z1, z] in W0

        proof

          (H . z) in ( field S) by A27, A49, A50, FUNCT_1:def 3;

          then

          consider z2 be object such that

           A51: [(H . z), z2] in S or [z2, (H . z)] in S by Th1;



           A52: [(H . z), z2] in S implies ex z1 be object st [z, z1] in W0 or [z1, z] in W0

          proof

            assume

             A53: [(H . z), z2] in S;

            then z2 in ( rng H) by A49, RELAT_1: 15;

            then

            consider z3 be object such that

             A54: z3 in ( dom H) and

             A55: z2 = (H . z3) by FUNCT_1:def 3;

            take z3;

             [z, z3] in [:M, M:] by A27, A50, A54, ZFMISC_1: 87;

            hence thesis by A29, A53, A55;

          end;

           [z2, (H . z)] in S implies ex z1 be object st [z, z1] in W0 or [z1, z] in W0

          proof

            assume

             A56: [z2, (H . z)] in S;

            then z2 in ( rng H) by A49, RELAT_1: 15;

            then

            consider z3 be object such that

             A57: z3 in ( dom H) and

             A58: z2 = (H . z3) by FUNCT_1:def 3;

            take z3;

             [z3, z] in [:M, M:] by A27, A50, A57, ZFMISC_1: 87;

            hence thesis by A29, A56, A58;

          end;

          hence thesis by A51, A52;

        end;

        hence thesis by Th1;

      end;

      then

       A59: ( field W0) = M by A36, TARSKI: 2;

      for a,b be object holds [a, b] in W0 iff a in ( field W0) & b in ( field W0) & [(H . a), (H . b)] in S

      proof

        let a,b be object;



         A60: [a, b] in W0 implies a in ( field W0) & b in ( field W0) & [(H . a), (H . b)] in S

        proof

          assume

           A61: [a, b] in W0;

          then

           A62: [a, b] in [:M, M:] by A29;

          consider x,y be object such that

           A63: [a, b] = [x, y] and

           A64: [(H . x), (H . y)] in S by A29, A61;

          a = x by A63, XTUPLE_0: 1;

          hence thesis by A59, A62, A63, A64, XTUPLE_0: 1, ZFMISC_1: 87;

        end;

        a in ( field W0) & b in ( field W0) & [(H . a), (H . b)] in S implies [a, b] in W0

        proof

          assume that

           A65: a in ( field W0) & b in ( field W0) and

           A66: [(H . a), (H . b)] in S;

           [a, b] in [:M, M:] by A59, A65, ZFMISC_1: 87;

          hence thesis by A29, A66;

        end;

        hence thesis by A60;

      end;

      then H is_isomorphism_of (W0,S) by A27, A35, A49, A59;

      then

       A67: (H " ) is_isomorphism_of (S,W0) by WELLORD1: 39;

      then W0 is well-ordering by A20, WELLORD1: 44;

      then

       A68: S1 is well-ordering by WELLORD1: 25;

      defpred P[ object] means ex x,y be object st $1 = [x, y] & [(H1 . x), (H1 . y)] in S1;

      consider W00 such that

       A69: for z be object holds z in W00 iff z in [:N, N:] & P[z] from XBOOLE_0:sch 1;

      for z be object st z in W00 holds ex x,y be object st z = [x, y]

      proof

        let z be object;

        assume z in W00;

        then ex z1,z2 be object st z = [z1, z2] & [(H1 . z1), (H1 . z2)] in S1 by A69;

        hence thesis;

      end;

      then

      reconsider W00 as Relation by RELAT_1:def 1;



       A70: for z be object holds z in ( field W00) implies z in N

      proof

        let z be object;

        assume z in ( field W00);

        then

        consider z1 be object such that

         A71: [z, z1] in W00 or [z1, z] in W00 by Th1;



         A72: [z1, z] in W00 implies z in N

        proof

          assume [z1, z] in W00;

          then [z1, z] in [:N, N:] by A69;

          hence thesis by ZFMISC_1: 87;

        end;

         [z, z1] in W00 implies z in N

        proof

          assume [z, z1] in W00;

          then [z, z1] in [:N, N:] by A69;

          hence thesis by ZFMISC_1: 87;

        end;

        hence thesis by A71, A72;

      end;

      ( rng H1) c= M

      proof

        let x be object;

        assume x in ( rng H1);

        then

        consider y be object such that

         A73: y in ( dom H1) and

         A74: x = (H1 . y) by FUNCT_1:def 3;

        for z1 be object holds z1 in {y} implies z1 in N by A41, A73, TARSKI:def 1;

        then

         A75: {y} c= N;

        x = {y} by A41, A42, A73, A74;

        hence thesis by A1, A75;

      end;

      then

       A76: ( field S1) = ( rng H1) by A20, A59, A67, WELLORD1: 31, WELLORD1: 44;

      for z be object holds z in N implies z in ( field W00)

      proof

        let z be object;

        assume

         A77: z in N;

        ex z1 be object st [z, z1] in W00 or [z1, z] in W00

        proof

          (H1 . z) in ( field S1) by A41, A76, A77, FUNCT_1:def 3;

          then

          consider z2 be object such that

           A78: [(H1 . z), z2] in S1 or [z2, (H1 . z)] in S1 by Th1;



           A79: [(H1 . z), z2] in S1 implies ex z1 be object st [z, z1] in W00 or [z1, z] in W00

          proof

            assume

             A80: [(H1 . z), z2] in S1;

            then z2 in ( rng H1) by A76, RELAT_1: 15;

            then

            consider z3 be object such that

             A81: z3 in ( dom H1) and

             A82: z2 = (H1 . z3) by FUNCT_1:def 3;

            take z3;

             [z, z3] in [:N, N:] by A41, A77, A81, ZFMISC_1: 87;

            hence thesis by A69, A80, A82;

          end;

           [z2, (H1 . z)] in S1 implies ex z1 be object st [z, z1] in W00 or [z1, z] in W00

          proof

            assume

             A83: [z2, (H1 . z)] in S1;

            then z2 in ( rng H1) by A76, RELAT_1: 15;

            then

            consider z3 be object such that

             A84: z3 in ( dom H1) and

             A85: z2 = (H1 . z3) by FUNCT_1:def 3;

            take z3;

             [z3, z] in [:N, N:] by A41, A77, A84, ZFMISC_1: 87;

            hence thesis by A69, A83, A85;

          end;

          hence thesis by A78, A79;

        end;

        hence thesis by Th1;

      end;

      then

       A86: ( field W00) = N by A70, TARSKI: 2;

      for a,b be object holds [a, b] in W00 iff a in ( field W00) & b in ( field W00) & [(H1 . a), (H1 . b)] in S1

      proof

        let a,b be object;



         A87: [a, b] in W00 implies a in ( field W00) & b in ( field W00) & [(H1 . a), (H1 . b)] in S1

        proof

          assume

           A88: [a, b] in W00;

          then

           A89: [a, b] in [:N, N:] by A69;

          consider x,y be object such that

           A90: [a, b] = [x, y] and

           A91: [(H1 . x), (H1 . y)] in S1 by A69, A88;

          a = x by A90, XTUPLE_0: 1;

          hence thesis by A86, A89, A90, A91, XTUPLE_0: 1, ZFMISC_1: 87;

        end;

        a in ( field W00) & b in ( field W00) & [(H1 . a), (H1 . b)] in S1 implies [a, b] in W00

        proof

          assume that

           A92: a in ( field W00) & b in ( field W00) and

           A93: [(H1 . a), (H1 . b)] in S1;

           [a, b] in [:N, N:] by A86, A92, ZFMISC_1: 87;

          hence thesis by A69, A93;

        end;

        hence thesis by A87;

      end;

      then H1 is_isomorphism_of (W00,S1) by A41, A47, A76, A86;

      then (H1 " ) is_isomorphism_of (S1,W00) by WELLORD1: 39;

      hence thesis by A68, A86, WELLORD1: 44;

    end;