ramsey_1.miz



    begin

    reserve n,m,k for Nat,

X,Y,Z for set,

f for Function of X, Y,

H for Subset of X;

    definition

      let X, Y, H;

      let P be a_partition of ( the_subsets_of_card (Y,X));

      :: RAMSEY_1:def1

      pred H is_homogeneous_for P means ex p be Element of P st ( the_subsets_of_card (Y,H)) c= p;

    end

    registration

      let n;

      let X be infinite set;

      cluster ( the_subsets_of_card (n,X)) -> non empty;

      correctness

      proof

         not ( card X) c= ( card n);

        hence thesis by GROUP_10: 1;

      end;

    end

    definition

      let n, X, Y, f;

      assume that

       A1: f is one-to-one and

       A2: ( card n) c= ( card X) & X is non empty and

       A3: Y is non empty;

      :: RAMSEY_1:def2

      func f ||^ n -> Function of ( the_subsets_of_card (n,X)), ( the_subsets_of_card (n,Y)) means

      : Def2: for x be Element of ( the_subsets_of_card (n,X)) holds (it . x) = (f .: x);

      existence

      proof

        set D = ( the_subsets_of_card (n,X));

        reconsider D as non empty set by A2, GROUP_10: 1;

        deffunc F( set) = (f .: $1);

        consider IT be Function such that

         A4: ( dom IT) = D & for x be Element of D holds (IT . x) = F(x) from FUNCT_1:sch 4;

        for y be object st y in ( rng IT) holds y in ( the_subsets_of_card (n,Y))

        proof

          let y be object;

          assume y in ( rng IT);

          then

          consider x be object such that

           A5: x in ( dom IT) and

           A6: y = (IT . x) by FUNCT_1:def 3;

          

           A7: ex x9 be Subset of X st x = x9 & ( card x9) = n by A4, A5;

          reconsider x as Element of D by A4, A5;

          

           A8: y = (f .: x) by A4, A6;

          f in ( Funcs (X,Y)) by A3, FUNCT_2: 8;

          then

           A9: ex f9 be Function st f = f9 & ( dom f9) = X & ( rng f9) c= Y by FUNCT_2:def 2;

          (f .: x) c= ( rng f) by RELAT_1: 111;

          then

          reconsider y9 = y as Subset of Y by A8, A9, XBOOLE_1: 1;

          (x,(f .: x)) are_equipotent by A1, A4, A5, A9, CARD_1: 33;

          then ( card y9) = n by A7, A8, CARD_1: 5;

          hence thesis;

        end;

        then ( rng IT) c= ( the_subsets_of_card (n,Y));

        then

        reconsider IT as Function of ( the_subsets_of_card (n,X)), ( the_subsets_of_card (n,Y)) by A4, FUNCT_2: 2;

        take IT;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( the_subsets_of_card (n,X)), ( the_subsets_of_card (n,Y)) such that

         A10: for x be Element of ( the_subsets_of_card (n,X)) holds (F1 . x) = (f .: x) and

         A11: for x be Element of ( the_subsets_of_card (n,X)) holds (F2 . x) = (f .: x);

        now

          let x be object;

          assume x in ( the_subsets_of_card (n,X));

          then

          reconsider x9 = x as Element of ( the_subsets_of_card (n,X));

          

          thus (F1 . x) = (f .: x9) by A10

          .= (F2 . x) by A11;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    

     Lm1: X c= Y implies ( the_subsets_of_card (Z,X)) c= ( the_subsets_of_card (Z,Y))

    proof

      assume

       A1: X c= Y;

      let x be object;

      assume x in ( the_subsets_of_card (Z,X));

      then

      consider x9 be Subset of X such that

       A2: x9 = x and

       A3: ( card x9) = Z;

      reconsider x99 = x9 as Subset of Y by A1, XBOOLE_1: 1;

      x99 = x by A2;

      hence thesis by A3;

    end;

    theorem :: RAMSEY_1:1

    

     Th1: f is one-to-one & ( card n) c= ( card X) & X is non empty & Y is non empty implies ( the_subsets_of_card (n,(f .: H))) = ((f ||^ n) .: ( the_subsets_of_card (n,H)))

    proof

      assume that

       A1: f is one-to-one and

       A2: ( card n) c= ( card X) and

       A3: X is non empty and

       A4: Y is non empty;

      consider f1 be Function such that

       A5: n c= (f1 .: X) by A2, CARD_1: 66;

      f in ( Funcs (X,Y)) by A4, FUNCT_2: 8;

      then

       A6: ex f9 be Function st f = f9 & ( dom f9) = X & ( rng f9) c= Y by FUNCT_2:def 2;

      then ( card X) c= ( card Y) by A1, CARD_1: 10;

      then

      consider f2 be Function such that

       A7: X c= (f2 .: Y) by CARD_1: 66;

      (f1 .: X) c= (f1 .: (f2 .: Y)) by A7, RELAT_1: 123;

      then n c= (f1 .: (f2 .: Y)) by A5;

      then n c= ((f1 * f2) .: Y) by RELAT_1: 126;

      then ( card n) c= ( card Y) by CARD_1: 66;

      then ( the_subsets_of_card (n,Y)) is non empty by A4, GROUP_10: 1;

      then (f ||^ n) in ( Funcs (( the_subsets_of_card (n,X)),( the_subsets_of_card (n,Y)))) by FUNCT_2: 8;

      then

       A8: ex fn be Function st (f ||^ n) = fn & ( dom fn) = ( the_subsets_of_card (n,X)) & ( rng fn) c= ( the_subsets_of_card (n,Y)) by FUNCT_2:def 2;

      for y be object holds y in ( the_subsets_of_card (n,(f .: H))) iff y in ((f ||^ n) .: ( the_subsets_of_card (n,H)))

      proof

        let y be object;

        hereby

          

           A9: (f .: H) c= ( rng f) by RELAT_1: 111;

          assume

           A10: y in ( the_subsets_of_card (n,(f .: H)));

          then

           A11: ex X9 be Subset of (f .: H) st y = X9 & ( card X9) = n;

          ex x be set st x in ( dom (f ||^ n)) & x in ( the_subsets_of_card (n,H)) & y = ((f ||^ n) . x)

          proof

            reconsider yy = y as set by TARSKI: 1;

            set x = (f " yy);

            take x;

            

             A12: x c= ( dom f) by RELAT_1: 132;

            

             A13: (f .: x) = y by A10, A9, FUNCT_1: 77, XBOOLE_1: 1;

            then

            reconsider x9 = x as Subset of H by A1, A10, A12, FUNCT_1: 87;

            (x,(f .: x)) are_equipotent by A1, A12, CARD_1: 33;

            then

             A14: ( card x9) = n by A11, A13, CARD_1: 5;

            then

             A15: x in ( the_subsets_of_card (n,H));

            

             A16: ( the_subsets_of_card (n,H)) c= ( the_subsets_of_card (n,X)) by Lm1;

            hence x in ( dom (f ||^ n)) by A8, A15;

            thus x in ( the_subsets_of_card (n,H)) by A14;

            

            thus y = (f .: x) by A10, A9, FUNCT_1: 77, XBOOLE_1: 1

            .= ((f ||^ n) . x) by A1, A2, A3, A4, A15, A16, Def2;

          end;

          hence y in ((f ||^ n) .: ( the_subsets_of_card (n,H))) by FUNCT_1:def 6;

        end;

        assume y in ((f ||^ n) .: ( the_subsets_of_card (n,H)));

        then

        consider x be object such that

         A17: x in ( dom (f ||^ n)) and

         A18: x in ( the_subsets_of_card (n,H)) and

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

        reconsider x as Element of ( the_subsets_of_card (n,X)) by A17;

        

         A20: y = (f .: x) by A1, A2, A3, A4, A19, Def2;

        then

        reconsider X9 = y as Subset of (f .: H) by A18, RELAT_1: 123;

        (ex x9 be Subset of H st x9 = x & ( card x9) = n) & (x,(f .: x)) are_equipotent by A1, A6, A18, CARD_1: 33, XBOOLE_1: 1;

        then ( card X9) = n by A20, CARD_1: 5;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    

     Lm2: ( the_subsets_of_card ( 0 ,X)) = { 0 }

    proof

      for x be object holds x in ( the_subsets_of_card ( 0 ,X)) iff x = 0

      proof

        let x be object;

        hereby

          assume x in ( the_subsets_of_card ( 0 ,X));

          then ex x9 be Subset of X st x9 = x & ( card x9) = 0 ;

          hence x = 0 ;

        end;

        assume

         A1: x = 0 ;

        then

        reconsider x9 = x as Subset of X by XBOOLE_1: 2;

        ( card x9) = 0 by A1;

        hence thesis;

      end;

      hence thesis by TARSKI:def 1;

    end;

    

     Lm3: for X,Y be finite set st ( card Y) = X holds ( the_subsets_of_card (X,Y)) = {Y}

    proof

      let X,Y be finite set;

      assume

       A1: ( card Y) = X;

      for x be object holds x in ( the_subsets_of_card (X,Y)) iff x = Y

      proof

        let x be object;

        hereby

          assume x in ( the_subsets_of_card (X,Y));

          then

          consider X9 be Subset of Y such that

           A2: X9 = x and

           A3: ( card X9) = X;

          reconsider X9 as finite Subset of Y;

          ( card (Y \ X9)) = (( card Y) - ( card X9)) by CARD_2: 44

          .= 0 by A1, A3;

          then (Y \ X9) = {} ;

          then Y c= X9 by XBOOLE_1: 37;

          hence x = Y by A2, XBOOLE_0:def 10;

        end;

        reconsider xx = x as set by TARSKI: 1;

        assume

         A4: x = Y;

        then xx c= Y;

        then

        reconsider x9 = x as Subset of Y;

        x9 in ( the_subsets_of_card (X,Y)) by A1, A4;

        hence thesis;

      end;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: RAMSEY_1:2

    

     Th2: X is infinite & X c= omega implies ( card X) = omega by WAYBEL12: 2, CARD_1: 5, CARD_1: 47;

    theorem :: RAMSEY_1:3

    

     Th3: X is infinite implies (X \/ Y) is infinite

    proof

      assume

       A1: X is infinite;

      

       A2: ( card X) c= ( card (X \/ Y)) by CARD_1: 11, XBOOLE_1: 7;

      assume (X \/ Y) is finite;

      hence contradiction by A1, A2;

    end;

    theorem :: RAMSEY_1:4

    

     Th4: X is infinite & Y is finite implies (X \ Y) is infinite

    proof

      assume

       A1: X is infinite & Y is finite;

      

       A2: (X \/ Y) = ((X \ Y) \/ Y) by XBOOLE_1: 39;

      assume (X \ Y) is finite;

      hence contradiction by A1, A2, Th3;

    end;

    registration

      let X be infinite set;

      let Y be set;

      cluster (X \/ Y) -> infinite;

      correctness by Th3;

    end

    registration

      let X be infinite set;

      let Y be finite set;

      cluster (X \ Y) -> infinite;

      correctness by Th4;

    end

    

     Lm4: for F be Function of ( the_subsets_of_card (n,X)), k st ( card X) = omega & X c= omega & k <> 0 holds ex H st H is infinite & (F | ( the_subsets_of_card (n,H))) is constant

    proof

      defpred P[ Nat] means for k be Nat, X be set, F be Function of ( the_subsets_of_card ($1,X)), k st ( card X) = omega & X c= omega & k <> 0 holds ex H be Subset of X st H is infinite & (F | ( the_subsets_of_card ($1,H))) is constant;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        now

          let k be Nat;

          let X be set;

          let F be Function of ( the_subsets_of_card ((n + 1),X)), k;

          assume

           A3: ( card X) = omega ;

          X c= X;

          then

           A4: X in ( the_subsets_of_card ( omega ,X)) by A3;

          then

          reconsider A = ( the_subsets_of_card ( omega ,X)) as non empty set;

          reconsider X0 = X as Element of A by A4;

          defpred P1[ set, set, set, set, set] means for x1,x2 be Element of A, y1,y2 be Element of omega st $2 = x1 & $3 = y1 & $4 = x2 & $5 = y2 holds (y1 in x1 implies (ex F1 be Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k, H1 be Subset of (x1 \ {y1}) st H1 is infinite & (F1 | ( the_subsets_of_card (n,H1))) is constant & x2 = H1 & y2 in H1 & y1 < y2 & (for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1}))) & for y29 be Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29)) & ( not y1 in x1 implies x2 = X & y2 = 0 );

          set Y0 = ( min* X);

          assume

           A5: X c= omega ;

          assume

           A6: k <> 0 ;

          

           A7: for Y be set, a be Element of Y st ( card Y) = omega & Y c= X holds ex Fa be Function of ( the_subsets_of_card (n,(Y \ {a}))), k, Ha be Subset of (Y \ {a}) st Ha is infinite & (Fa | ( the_subsets_of_card (n,Ha))) is constant & for Y9 be Element of ( the_subsets_of_card (n,(Y \ {a}))) holds (Fa . Y9) = (F . (Y9 \/ {a}))

          proof

            let Y be set;

            let a be Element of Y;

            set Y1 = ( the_subsets_of_card (n,(Y \ {a})));

            assume

             A8: ( card Y) = omega ;

            then

             A9: Y is infinite;

            then

            reconsider Y1 as non empty set;

            deffunc F1( Element of Y1) = (F . ($1 \/ {a}));

            assume

             A10: Y c= X;

            Y is non empty by A8;

            then

             A11: {a} c= Y by ZFMISC_1: 31;

            

             A12: for x be Element of Y1 holds F1(x) in k

            proof

              let x be Element of Y1;

              x in Y1;

              then

              consider x9 be Subset of (Y \ {a}) such that

               A13: x = x9 and

               A14: ( card x9) = n;

              (x \/ {a}) c= ((Y \ {a}) \/ {a}) by A13, XBOOLE_1: 9;

              then (x \/ {a}) c= (Y \/ {a}) by XBOOLE_1: 39;

              then

              reconsider y = (x \/ {a}) as Subset of Y by A11, XBOOLE_1: 12;

              reconsider x99 = x9 as finite set by A14;

               not a in x99

              proof

                assume a in x99;

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

                hence contradiction by TARSKI:def 1;

              end;

              then ( card y) = (n + 1) by A13, A14, CARD_2: 41;

              then

               A15: (x \/ {a}) in ( the_subsets_of_card ((n + 1),Y));

              ( the_subsets_of_card ((n + 1),Y)) c= ( the_subsets_of_card ((n + 1),X)) by A10, Lm1;

              hence thesis by A6, A15, FUNCT_2: 5;

            end;

            consider Fa be Function of Y1, k such that

             A16: for x be Element of Y1 holds (Fa . x) = F1(x) from FUNCT_2:sch 8( A12);

            reconsider Fa as Function of ( the_subsets_of_card (n,(Y \ {a}))), k;

            

             A17: Y c= omega by A5, A10;

            then ( card (Y \ {a})) = omega by A9, Th2, XBOOLE_1: 1;

            then

            consider Ha be Subset of (Y \ {a}) such that

             A18: Ha is infinite & (Fa | ( the_subsets_of_card (n,Ha))) is constant by A2, A6, A17, XBOOLE_1: 1;

            take Fa, Ha;

            thus Ha is infinite & (Fa | ( the_subsets_of_card (n,Ha))) is constant by A18;

            let Y9 be Element of ( the_subsets_of_card (n,(Y \ {a})));

            thus thesis by A16;

          end;

          

           A19: for a be Nat, x99 be Element of A, y99 be Element of omega holds ex x199 be Element of A, y199 be Element of omega st P1[a, x99, y99, x199, y199]

          proof

            let a be Nat;

            let x99 be Element of A;

            let y99 be Element of omega ;

            per cases ;

              suppose

               A20: y99 in x99;

              then

              reconsider a9 = y99 as Element of x99;

              

               A21: x99 in A;

              then ex x999 be Subset of X st x999 = x99 & ( card x999) = omega ;

              then

              consider Fa be Function of ( the_subsets_of_card (n,(x99 \ {a9}))), k, Ha be Subset of (x99 \ {a9}) such that

               A22: Ha is infinite and

               A23: (Fa | ( the_subsets_of_card (n,Ha))) is constant and

               A24: for Y9 be Element of ( the_subsets_of_card (n,(x99 \ {a9}))) holds (Fa . Y9) = (F . (Y9 \/ {a9})) by A7;

              Ha c= x99 by XBOOLE_1: 1;

              then

               A25: Ha c= X by A21, XBOOLE_1: 1;

              then ( card Ha) = omega by A5, A22, Th2, XBOOLE_1: 1;

              then Ha in A by A25;

              then

              reconsider x199 = Ha as Element of A;

              set y199 = ( min* { y29 where y29 be Element of omega : y29 > y99 & y29 in Ha });

              take x199, y199;

              

               A26: Ha c= omega by A5, A25;

              now

                let x1,x2 be Element of A;

                let y1,y2 be Element of omega ;

                assume that

                 A27: x99 = x1 and

                 A28: y99 = y1;

                assume that

                 A29: x199 = x2 and

                 A30: y199 = y2;

                thus y1 in x1 implies ex F1 be Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k, H1 be Subset of (x1 \ {y1}) st H1 is infinite & (F1 | ( the_subsets_of_card (n,H1))) is constant & x2 = H1 & y2 in H1 & y1 < y2 & (for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1}))) & for y29 be Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29

                proof

                  reconsider H1 = Ha as Subset of (x1 \ {y1}) by A27, A28;

                  set A9 = { y29 where y29 be Element of omega : y29 > y99 & y29 in Ha };

                  reconsider F1 = Fa as Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k by A27, A28;

                  assume y1 in x1;

                  take F1, H1;

                  for x be object st x in A9 holds x in NAT

                  proof

                    let x be object;

                    assume x in A9;

                    then ex x9 be Element of omega st x9 = x & x9 > y99 & x9 in Ha;

                    hence thesis;

                  end;

                  then

                  reconsider A9 as Subset of NAT by TARSKI:def 3;

                  thus H1 is infinite by A22;

                  thus (F1 | ( the_subsets_of_card (n,H1))) is constant by A23;

                  thus x2 = H1 by A29;

                  A9 <> {}

                  proof

                    set A99 = { y2999 where y2999 be Element of omega : y2999 <= y99 & y2999 in Ha };

                     A31:

                    now

                      let x be object;

                      assume

                       A32: x in (A9 \/ A99);

                      per cases by A32, XBOOLE_0:def 3;

                        suppose x in A9;

                        then ex x9 be Element of omega st x = x9 & x9 > y99 & x9 in Ha;

                        hence x in Ha;

                      end;

                        suppose x in A99;

                        then ex x9 be Element of omega st x = x9 & x9 <= y99 & x9 in Ha;

                        hence x in Ha;

                      end;

                    end;

                    now

                      let x be object;

                      assume x in A99;

                      then

                      consider x9 be Element of omega such that

                       A33: x = x9 and

                       A34: x9 <= y99 and x9 in Ha;

                      x9 < (y99 + 1) by A34, NAT_1: 13;

                      hence x in ( Segm (y99 + 1)) by A33, NAT_1: 44;

                    end;

                    then

                     A35: A99 c= ( Segm (y99 + 1));

                     A36:

                    now

                      let x be object;

                      assume

                       A37: x in Ha;

                      then

                      reconsider x9 = x as Element of omega by A26;

                      per cases ;

                        suppose x9 <= y99;

                        then x in A99 by A37;

                        hence x in (A9 \/ A99) by XBOOLE_0:def 3;

                      end;

                        suppose x9 > y99;

                        then x in A9 by A37;

                        hence x in (A9 \/ A99) by XBOOLE_0:def 3;

                      end;

                    end;

                    assume A9 = {} ;

                    hence contradiction by A22, A35, A31, A36, TARSKI: 2;

                  end;

                  then y199 in A9 by NAT_1:def 1;

                  then

                   A38: ex y299 be Element of omega st y199 = y299 & y299 > y99 & y299 in Ha;

                  hence y2 in H1 by A30;

                  thus y1 < y2 by A28, A30, A38;

                  thus for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1})) by A24, A27, A28;

                  let y29 be Element of omega ;

                  assume

                   A39: y29 > y1;

                  assume y29 in H1;

                  then y29 in A9 by A28, A39;

                  hence thesis by A30, NAT_1:def 1;

                end;

                assume not y1 in x1;

                hence thesis by A20, A27, A28;

              end;

              hence thesis;

            end;

              suppose

               A40: not y99 in x99;

              reconsider y199 = 0 as Element of omega ;

              reconsider x199 = X as Element of A by A4;

              take x199, y199;

              thus thesis by A40;

            end;

          end;

          consider S be sequence of A, a be sequence of omega such that

           A41: (S . 0 ) = X0 & (a . 0 ) = Y0 & for i be Nat holds P1[i, (S . i), (a . i), (S . (i + 1)), (a . (i + 1))] from RECDEF_2:sch 3( A19);

          defpred P2[ Nat] means (a . $1) in ( Segm (a . ($1 + 1))) & (S . ($1 + 1)) c= (S . $1) & (a . $1) in (S . $1) & (a . ($1 + 1)) in (S . ($1 + 1)) & not (a . $1) in (S . ($1 + 1));

          

           A42: P2[ 0 ]

          proof

            set i = 0 ;

            reconsider i as Element of NAT ;

            reconsider x1 = (S . i) as Element of A;

            reconsider x2 = (S . (i + 1)) as Element of A;

            reconsider y1 = (a . i) as Element of omega ;

            reconsider y2 = (a . (i + 1)) as Element of omega ;

            

             A43: y1 in x1 implies ex F1 be Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k, H1 be Subset of (x1 \ {y1}) st H1 is infinite & (F1 | ( the_subsets_of_card (n,H1))) is constant & x2 = H1 & y2 in H1 & y1 < y2 & (for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1}))) & for y29 be Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 by A41;

            hence (a . 0 ) in ( Segm (a . ( 0 + 1))) by A3, A5, A41, CARD_1: 27, NAT_1: 44, NAT_1:def 1;

            thus (S . ( 0 + 1)) c= (S . 0 ) by A3, A5, A41, A43, CARD_1: 27, NAT_1:def 1, XBOOLE_1: 1;

            thus (a . 0 ) in (S . 0 ) by A3, A5, A41, CARD_1: 27, NAT_1:def 1;

            thus (a . ( 0 + 1)) in (S . ( 0 + 1)) by A3, A5, A41, A43, CARD_1: 27, NAT_1:def 1;

             not y1 in x2

            proof

              assume y1 in x2;

              then not y1 in {y1} by A3, A5, A41, A43, CARD_1: 27, NAT_1:def 1, XBOOLE_0:def 5;

              hence contradiction by TARSKI:def 1;

            end;

            hence thesis;

          end;

          defpred P4[ object, object] means for Y be set, i be Element of NAT , Fi be Function of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))), k st i = $1 & Y = { x where x be Element of omega : ex j be Element of NAT st (a . j) = x & j > i } & (for Y9 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (Fi . Y9) = (F . (Y9 \/ {(a . i)}))) holds ex l be Nat st l = $2 & l in k & ( rng (Fi | ( the_subsets_of_card (n,Y)))) = {l};

          defpred P3[ Nat] means for i,j be Nat st i >= j & i = ($1 + j) holds (S . i) c= (S . j) & (for ai,aj be Nat st i <> j & ai = (a . i) & aj = (a . j) holds ai > aj);

          

           A44: for i be Nat st P2[i] holds P2[(i + 1)]

          proof

            let i be Nat;

            reconsider i9 = (i + 1) as Element of NAT ;

            reconsider x1 = (S . i9) as Element of A;

            reconsider x2 = (S . (i9 + 1)) as Element of A;

            reconsider y1 = (a . i9) as Element of omega ;

            reconsider y2 = (a . (i9 + 1)) as Element of omega ;

            assume

             A45: P2[i];

            then

             A46: ex F1 be Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k, H1 be Subset of (x1 \ {y1}) st H1 is infinite & (F1 | ( the_subsets_of_card (n,H1))) is constant & x2 = H1 & y2 in H1 & y1 < y2 & (for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1}))) & for y29 be Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 by A41;

             not y1 in x2

            proof

              assume y1 in x2;

              then not y1 in {y1} by A46, XBOOLE_0:def 5;

              hence contradiction by TARSKI:def 1;

            end;

            hence P2[(i + 1)] by A45, A46, NAT_1: 44, XBOOLE_1: 1;

          end;

          

           A47: for i be Nat holds P2[i] from NAT_1:sch 2( A42, A44);

          

           A48: for l be Nat st P3[l] holds P3[(l + 1)]

          proof

            let l be Nat;

            assume

             A49: P3[l];

            thus P3[(l + 1)]

            proof

              let i,j be Nat;

              assume

               A50: i >= j;

              set j9 = (j + 1);

              assume

               A51: i = ((l + 1) + j);

              then

               A52: i = (l + j9);

              

               A53: (S . (j + 1)) c= (S . j) by A47;

              i <> j

              proof

                assume i = j;

                then 0 = (l + 1) by A51;

                hence contradiction;

              end;

              then i > j by A50, XXREAL_0: 1;

              then

               A54: i >= j9 by NAT_1: 13;

              then (S . i) c= (S . (j + 1)) by A49, A52;

              hence (S . i) c= (S . j) by A53;

              

               A55: for ai,aj9 be Nat st i <> j9 & ai = (a . i) & aj9 = (a . j9) holds ai > aj9 by A49, A54, A52;

              thus for ai,aj be Nat st i <> j & ai = (a . i) & aj = (a . j) holds ai > aj

              proof

                let ai,aj be Nat;

                assume i <> j;

                assume that

                 A56: ai = (a . i) and

                 A57: aj = (a . j);

                reconsider aj9 = (a . j9) as Nat;

                aj in ( Segm aj9) by A47, A57;

                then aj9 > aj by NAT_1: 44;

                hence thesis by A55, A56, XXREAL_0: 2;

              end;

            end;

          end;

          

           A58: P3[ 0 ];

          

           A59: for l be Nat holds P3[l] from NAT_1:sch 2( A58, A48);

          

           A60: for i,j be Nat st i >= j holds (S . i) c= (S . j) & for ai,aj be Nat st i <> j & ai = (a . i) & aj = (a . j) holds ai > aj

          proof

            let i,j be Nat;

            assume

             A61: i >= j;

            then

             A62: ex l be Nat st i = (j + l) by NAT_1: 10;

            hence (S . i) c= (S . j) by A59, A61;

            thus thesis by A59, A61, A62;

          end;

          

           A63: for i be Element of NAT , Y be set, Fi be Function of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))), k st Y = { x where x be Element of omega : ex j be Element of NAT st (a . j) = x & j > i } & (for Y9 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (Fi . Y9) = (F . (Y9 \/ {(a . i)}))) holds Y c= (S . (i + 1)) & (Fi | ( the_subsets_of_card (n,Y))) is constant

          proof

            let i be Element of NAT ;

            let Y be set;

            let Fi be Function of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))), k;

            assume

             A64: Y = { x where x be Element of omega : ex j be Element of NAT st (a . j) = x & j > i };

            consider x2 be Element of A, y2 be Element of omega such that

             A65: (S . (i + 1)) = x2 and

             A66: (a . (i + 1)) = y2;

            consider x1 be Element of A, y1 be Element of omega such that

             A67: (S . i) = x1 & (a . i) = y1;

            y1 in x1 implies (ex F1 be Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k, H1 be Subset of (x1 \ {y1}) st H1 is infinite & (F1 | ( the_subsets_of_card (n,H1))) is constant & x2 = H1 & y2 in H1 & y1 < y2 & (for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1}))) & for y29 be Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29) & ( not y1 in x1 implies x2 = X & y2 = 0 ) by A41, A67, A65, A66;

            then

            consider F1 be Function of ( the_subsets_of_card (n,(x1 \ {y1}))), k, H1 be Subset of (x1 \ {y1}) such that H1 is infinite and

             A68: (F1 | ( the_subsets_of_card (n,H1))) is constant & x2 = H1 and

             A69: for x19 be Element of ( the_subsets_of_card (n,(x1 \ {y1}))) holds (F1 . x19) = (F . (x19 \/ {y1})) and for y29 be Element of omega st y29 > y1 & y29 in H1 holds y2 <= y29 by A47, A67;

            reconsider F1 as Function of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))), k by A67;

            assume

             A70: for Y9 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (Fi . Y9) = (F . (Y9 \/ {(a . i)}));

            for x19 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (F1 . x19) = (Fi . x19)

            proof

              let x19 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)})));

              

              thus (F1 . x19) = (F . (x19 \/ {(a . i)})) by A67, A69

              .= (Fi . x19) by A70;

            end;

            then

             A71: (Fi | ( the_subsets_of_card (n,(S . (i + 1))))) is constant by A65, A68, FUNCT_2: 63;

            now

              let x be object;

              assume x in Y;

              then ex x9 be Element of omega st x = x9 & ex j be Element of NAT st (a . j) = x9 & j > i by A64;

              then

              consider j be Element of NAT such that

               A72: (a . j) = x and

               A73: j > i;

              j >= (i + 1) by A73, NAT_1: 13;

              then

               A74: (S . j) c= (S . (i + 1)) by A60;

              (a . j) in (S . j) by A47;

              hence x in (S . (i + 1)) by A72, A74;

            end;

            hence Y c= (S . (i + 1));

            then

             A75: ( the_subsets_of_card (n,Y)) c= ( the_subsets_of_card (n,(S . (i + 1)))) by Lm1;

            for x,y be object st x in ( dom (Fi | ( the_subsets_of_card (n,Y)))) & y in ( dom (Fi | ( the_subsets_of_card (n,Y)))) holds ((Fi | ( the_subsets_of_card (n,Y))) . x) = ((Fi | ( the_subsets_of_card (n,Y))) . y)

            proof

              let x,y be object;

              assume

               A76: x in ( dom (Fi | ( the_subsets_of_card (n,Y))));

              then

               A77: x in ( the_subsets_of_card (n,Y));

              x in ( dom Fi) by A76, RELAT_1: 57;

              then

               A78: x in ( dom (Fi | ( the_subsets_of_card (n,(S . (i + 1)))))) by A75, A77, RELAT_1: 57;

              assume

               A79: y in ( dom (Fi | ( the_subsets_of_card (n,Y))));

              then

               A80: y in ( the_subsets_of_card (n,Y));

              y in ( dom Fi) by A79, RELAT_1: 57;

              then

               A81: y in ( dom (Fi | ( the_subsets_of_card (n,(S . (i + 1)))))) by A75, A80, RELAT_1: 57;

              

              thus ((Fi | ( the_subsets_of_card (n,Y))) . x) = (((Fi | ( the_subsets_of_card (n,(S . (i + 1))))) | ( the_subsets_of_card (n,Y))) . x) by A75, FUNCT_1: 51

              .= ((Fi | ( the_subsets_of_card (n,(S . (i + 1))))) . x) by A77, FUNCT_1: 49

              .= ((Fi | ( the_subsets_of_card (n,(S . (i + 1))))) . y) by A71, A78, A81, FUNCT_1:def 10

              .= (((Fi | ( the_subsets_of_card (n,(S . (i + 1))))) | ( the_subsets_of_card (n,Y))) . y) by A80, FUNCT_1: 49

              .= ((Fi | ( the_subsets_of_card (n,Y))) . y) by A75, FUNCT_1: 51;

            end;

            hence thesis by FUNCT_1:def 10;

          end;

          for x1,x2 be object st x1 in ( dom a) & x2 in ( dom a) & (a . x1) = (a . x2) holds x1 = x2

          proof

            let x1,x2 be object;

            assume x1 in ( dom a);

            then

            reconsider i1 = x1 as Element of NAT ;

            assume x2 in ( dom a);

            then

            reconsider i2 = x2 as Element of NAT ;

            reconsider ai2 = (a . i2) as Element of NAT ;

            reconsider ai1 = (a . i1) as Element of NAT ;

            assume

             A82: (a . x1) = (a . x2);

            assume

             A83: x1 <> x2;

            per cases by A83, XXREAL_0: 1;

              suppose i1 < i2;

              then ai1 < ai2 by A60;

              hence contradiction by A82;

            end;

              suppose i1 > i2;

              then ai1 > ai2 by A60;

              hence contradiction by A82;

            end;

          end;

          then

           A84: a is one-to-one by FUNCT_1:def 4;

          

           A85: NAT = ( dom a) by FUNCT_2:def 1;

          

           A86: for i be Element of NAT holds ( card { x9 where x9 be Element of omega : ex j be Element of NAT st (a . j) = x9 & j > i }) = omega

          proof

            let i be Element of NAT ;

            set Z = { x9 where x9 be Element of omega : ex j be Element of NAT st (a . j) = x9 & j > i };

            now

              let z be object;

              assume z in Z;

              then ex z9 be Element of omega st z = z9 & ex j be Element of NAT st (a . j) = z9 & j > i;

              hence z in NAT ;

            end;

            then

             A87: Z c= NAT ;

            

             A88: ( dom (a | ( NAT \ ( Segm (i + 1))))) = (( dom a) /\ ( NAT \ ( Segm (i + 1)))) by RELAT_1: 61

            .= ( NAT /\ ( NAT \ ( Segm (i + 1)))) by FUNCT_2:def 1

            .= (( NAT /\ NAT ) \ ( Segm (i + 1))) by XBOOLE_1: 49

            .= ( NAT \ ( Segm (i + 1)));

            for z be object holds z in Z iff z in ( rng (a | ( NAT \ ( Segm (i + 1)))))

            proof

              let z be object;

              hereby

                assume z in Z;

                then ex z9 be Element of omega st z = z9 & ex j be Element of NAT st (a . j) = z9 & j > i;

                then

                consider j be Element of NAT such that

                 A89: (a . j) = z and

                 A90: j > i;

                j >= (i + 1) by A90, NAT_1: 13;

                then not j in ( Segm (i + 1)) by NAT_1: 44;

                then j in ( NAT \ ( Segm (i + 1))) by XBOOLE_0:def 5;

                hence z in ( rng (a | ( NAT \ ( Segm (i + 1))))) by A85, A89, FUNCT_1: 50;

              end;

              assume z in ( rng (a | ( NAT \ ( Segm (i + 1)))));

              then

              consider j be object such that

               A91: j in ( dom (a | ( NAT \ ( Segm (i + 1))))) and

               A92: z = ((a | ( NAT \ ( Segm (i + 1)))) . j) by FUNCT_1:def 3;

              j in ( dom a) by A91, RELAT_1: 57;

              then

              reconsider j as Element of NAT ;

              ( dom (a | ( NAT \ ( Segm (i + 1))))) c= ( NAT \ ( Segm (i + 1))) by RELAT_1: 58;

              then not j in ( Segm (i + 1)) by A91, XBOOLE_0:def 5;

              then j >= (i + 1) by NAT_1: 44;

              then

               A93: j > i by NAT_1: 13;

              (a . j) = z by A91, A92, FUNCT_1: 47;

              hence thesis by A93;

            end;

            then

             A94: Z = ( rng (a | ( NAT \ ( Segm (i + 1))))) by TARSKI: 2;

            (a | ( NAT \ ( Segm (i + 1)))) is one-to-one by A84, FUNCT_1: 52;

            hence thesis by A88, A94, A87, Th2, CARD_1: 59;

          end;

          

           A95: for x be object st x in NAT holds ex y be object st y in k & P4[x, y]

          proof

            let x be object;

            assume x in NAT ;

            then

            reconsider i9 = x as Element of NAT ;

            set Y9 = (S . i9);

            

             A96: not (a . i9) in (S . (i9 + 1)) by A47;

            reconsider a9 = (a . i9) as Element of Y9 by A47;

            set Z = { x9 where x9 be Element of omega : ex j be Element of NAT st (a . j) = x9 & j > i9 };

            

             A97: (S . (i9 + 1)) c= (S . i9) by A47;

            Y9 in A;

            then ex Y99 be Subset of X st Y99 = Y9 & ( card Y99) = omega ;

            then

            consider Fa be Function of ( the_subsets_of_card (n,(Y9 \ {a9}))), k, Ha be Subset of (Y9 \ {a9}) such that Ha is infinite and (Fa | ( the_subsets_of_card (n,Ha))) is constant and

             A98: for Y99 be Element of ( the_subsets_of_card (n,(Y9 \ {a9}))) holds (Fa . Y99) = (F . (Y99 \/ {a9})) by A7;

            

             A99: Z c= (S . (i9 + 1)) by A63, A98;

            now

              let x be object;

              assume x in Z;

              then

               A100: x in (S . (i9 + 1)) by A99;

              then not x in {(a . i9)} by A96, TARSKI:def 1;

              hence x in ((S . i9) \ {(a . i9)}) by A97, A100, XBOOLE_0:def 5;

            end;

            then Z c= ((S . i9) \ {(a . i9)});

            then ( the_subsets_of_card (n,Z)) c= ( the_subsets_of_card (n,(Y9 \ {a9}))) by Lm1;

            then

             A101: (Fa | ( the_subsets_of_card (n,Z))) is Function of ( the_subsets_of_card (n,Z)), k by A6, FUNCT_2: 32;

            

             A102: not ( card Z) c= ( card n) by A86;

            then Z is non empty;

            then

             A103: ( the_subsets_of_card (n,Z)) is non empty by A102, GROUP_10: 1;

            (Fa | ( the_subsets_of_card (n,Z))) is constant by A63, A98;

            then

            consider y be Element of k such that

             A104: ( rng (Fa | ( the_subsets_of_card (n,Z)))) = {y} by A6, A101, A103, FUNCT_2: 111;

            reconsider y as set;

            take y;

            thus y in k by A6;

            for Y be set, i be Element of NAT , Fi be Function of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))), k st i = x & Y = { x9 where x9 be Element of omega : ex j be Element of NAT st (a . j) = x9 & j > i } & (for Y9 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (Fi . Y9) = (F . (Y9 \/ {(a . i)}))) holds ex l be Nat st l = y & l in k & ( rng (Fi | ( the_subsets_of_card (n,Y)))) = {l}

            proof

              reconsider k9 = k as Element of NAT by ORDINAL1:def 12;

              let Y be set;

              let i be Element of NAT ;

              let Fi be Function of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))), k;

              assume

               A105: i = x;

              k9 is Subset of NAT by STIRL2_1: 8;

              then

              reconsider l = y as Nat;

              assume

               A106: Y = { x9 where x9 be Element of omega : ex j be Element of NAT st (a . j) = x9 & j > i };

              assume

               A107: for Y9 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (Fi . Y9) = (F . (Y9 \/ {(a . i)}));

              take l;

              thus l = y;

              thus l in k by A6;

              for x19 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)}))) holds (Fa . x19) = (Fi . x19)

              proof

                let x19 be Element of ( the_subsets_of_card (n,((S . i) \ {(a . i)})));

                

                thus (Fa . x19) = (F . (x19 \/ {(a . i)})) by A98, A105

                .= (Fi . x19) by A107;

              end;

              hence thesis by A104, A105, A106, FUNCT_2: 63;

            end;

            hence P4[x, y];

          end;

          consider g be sequence of k such that

           A108: for x be object st x in NAT holds P4[x, (g . x)] from FUNCT_2:sch 1( A95);

          g in ( Funcs ( NAT ,k)) by A6, FUNCT_2: 8;

          then ex g9 be Function st g = g9 & ( dom g9) = NAT & ( rng g9) c= k by FUNCT_2:def 2;

          then

          consider k9 be object such that k9 in ( rng g) and

           A109: (g " {k9}) is infinite by CARD_2: 101;

          set H = (a .: (g " {k9}));

          (g " {k9}) c= ( dom g) by RELAT_1: 132;

          then ((g " {k9}),H) are_equipotent by A84, A85, CARD_1: 33, XBOOLE_1: 1;

          then

           A110: ( card (g " {k9})) = ( card H) by CARD_1: 5;

          now

            let y be object;

            assume y in H;

            then

            consider x be object such that

             A111: [x, y] in a and x in (g " {k9}) by RELAT_1:def 13;

            x in ( dom a) by A111, FUNCT_1: 1;

            then

            reconsider i = x as Element of NAT ;

            y = (a . x) by A111, FUNCT_1: 1;

            then

             A112: y in (S . i) by A47;

            (S . i) in ( the_subsets_of_card ( omega ,X));

            hence y in X by A112;

          end;

          then

          reconsider H as Subset of X by TARSKI:def 3;

          take H;

          thus H is infinite by A109, A110;

          

           A113: for y be set st y in ( dom (F | ( the_subsets_of_card ((n + 1),H)))) holds ((F | ( the_subsets_of_card ((n + 1),H))) . y) = k9

          proof

            let y be set;

            assume y in ( dom (F | ( the_subsets_of_card ((n + 1),H))));

            then

             A114: y in ( the_subsets_of_card ((n + 1),H)) by RELAT_1: 57;

            then

            consider Y be Subset of H such that

             A115: y = Y and

             A116: ( card Y) = (n + 1);

            set y0 = ( min* Y);

            set Y9 = (y \ {y0});

            Y c= X by XBOOLE_1: 1;

            then

             A117: Y c= NAT by A5;

            then

             A118: y0 in Y by A116, CARD_1: 27, NAT_1:def 1;

            then

            consider x0 be object such that x0 in ( dom a) and

             A119: x0 in (g " {k9}) and

             A120: y0 = (a . x0) by FUNCT_1:def 6;

            consider y09 be object such that y09 in ( rng g) and

             A121: [x0, y09] in g and

             A122: y09 in {k9} by A119, RELAT_1: 131;

            

             A123: x0 in ( dom g) by A121, FUNCT_1: 1;

            

             A124: (g . x0) = y09 by A121, FUNCT_1: 1;

            reconsider x0 as Element of NAT by A123;

            set Y0 = { x where x be Element of omega : ex j be Element of NAT st (a . j) = x & j > x0 };

             {y0} c= y by A115, A118, ZFMISC_1: 31;

            then

             A125: (Y9 \/ {(a . x0)}) = y by A120, XBOOLE_1: 45;

            reconsider a9 = (a . x0) as Element of (S . x0) by A47;

            (S . x0) in ( the_subsets_of_card ( omega ,X));

            then ex S0 be Subset of X st S0 = (S . x0) & ( card S0) = omega ;

            then

            consider F0 be Function of ( the_subsets_of_card (n,((S . x0) \ {a9}))), k, H0 be Subset of ((S . x0) \ {a9}) such that H0 is infinite and (F0 | ( the_subsets_of_card (n,H0))) is constant and

             A126: for Y9 be Element of ( the_subsets_of_card (n,((S . x0) \ {a9}))) holds (F0 . Y9) = (F . (Y9 \/ {a9})) by A7;

            reconsider y9 = y as finite set by A115, A116;

            ( card Y9) c= ( card y9) by CARD_1: 11;

            then

            reconsider Y99 = Y9 as finite set;

            

             A127: Y0 c= (S . (x0 + 1)) by A63, A126;

            now

              let x be object;

              assume

               A128: x in Y9;

              then

               A129: x in y;

              then

              consider j be object such that

               A130: j in ( dom a) and j in (g " {k9}) and

               A131: x = (a . j) by A115, FUNCT_1:def 6;

              reconsider x9 = x as Element of omega by A115, A117, A129;

              

               A132: not x in {y0} by A128, XBOOLE_0:def 5;

              ex j be Element of NAT st (a . j) = x9 & j > x0

              proof

                reconsider j as Element of NAT by A130;

                take j;

                thus (a . j) = x9 by A131;

                

                 A133: y0 <= x9 by A115, A117, A128, NAT_1:def 1;

                thus j > x0

                proof

                  assume

                   A134: x0 >= j;

                  x0 <> j by A120, A132, A131, TARSKI:def 1;

                  hence contradiction by A60, A120, A131, A133, A134;

                end;

              end;

              hence x in Y0;

            end;

            then

             A135: Y9 is Subset of Y0 by TARSKI:def 3;

            y0 in {y0} by TARSKI:def 1;

            then not (a . x0) in Y9 by A120, XBOOLE_0:def 5;

            then ( card y9) = (( card Y99) + 1) by A125, CARD_2: 41;

            then

             A136: Y9 in ( the_subsets_of_card (n,Y0)) by A115, A116, A135;

            ex l be Nat st l = (g . x0) & l in k & ( rng (F0 | ( the_subsets_of_card (n,Y0)))) = {l} by A108, A126;

            then

             A137: ( rng (F0 | ( the_subsets_of_card (n,Y0)))) = {k9} by A122, A124, TARSKI:def 1;

            (S . (x0 + 1)) c= (S . x0) by A47;

            then Y0 c= (S . x0) by A127;

            then

             A138: (Y0 \ {(a . x0)}) c= ((S . x0) \ {(a . x0)}) by XBOOLE_1: 33;

             not (a . x0) in Y0 by A47, A127;

            then Y0 c= ((S . x0) \ {(a . x0)}) by A138, ZFMISC_1: 57;

            then

             A139: ( the_subsets_of_card (n,Y0)) c= ( the_subsets_of_card (n,((S . x0) \ {(a . x0)}))) by Lm1;

            then

             A140: Y9 in ( the_subsets_of_card (n,((S . x0) \ {(a . x0)}))) by A136;

            reconsider Y9 as Element of ( the_subsets_of_card (n,((S . x0) \ {(a . x0)}))) by A139, A136;

            Y9 in ( dom F0) by A6, A140, FUNCT_2:def 1;

            then Y9 in ( dom (F0 | ( the_subsets_of_card (n,Y0)))) by A136, RELAT_1: 57;

            then ((F0 | ( the_subsets_of_card (n,Y0))) . Y9) in ( rng (F0 | ( the_subsets_of_card (n,Y0)))) by FUNCT_1: 3;

            then ((F0 | ( the_subsets_of_card (n,Y0))) . Y9) = k9 by A137, TARSKI:def 1;

            then

             A141: (F0 . Y9) = k9 by A136, FUNCT_1: 49;

            (F0 . Y9) = (F . (Y9 \/ {(a . x0)})) by A126;

            hence thesis by A114, A125, A141, FUNCT_1: 49;

          end;

          for x,y be object st x in ( dom (F | ( the_subsets_of_card ((n + 1),H)))) & y in ( dom (F | ( the_subsets_of_card ((n + 1),H)))) holds ((F | ( the_subsets_of_card ((n + 1),H))) . x) = ((F | ( the_subsets_of_card ((n + 1),H))) . y)

          proof

            let x,y be object;

            assume x in ( dom (F | ( the_subsets_of_card ((n + 1),H))));

            then

             A142: ((F | ( the_subsets_of_card ((n + 1),H))) . x) = k9 by A113;

            assume y in ( dom (F | ( the_subsets_of_card ((n + 1),H))));

            hence thesis by A113, A142;

          end;

          hence (F | ( the_subsets_of_card ((n + 1),H))) is constant by FUNCT_1:def 10;

        end;

        hence thesis;

      end;

      

       A143: P[ 0 ]

      proof

        let k be Nat;

        let X be set;

        set H = X;

        H c= X;

        then

        reconsider H as Subset of X;

        let F be Function of ( the_subsets_of_card ( 0 ,X)), k;

        assume

         A144: ( card X) = omega ;

        assume X c= omega ;

        assume k <> 0 ;

        take H;

        thus H is infinite by A144;

        for x,y be object holds x in ( dom (F | ( the_subsets_of_card ( 0 ,H)))) & y in ( dom (F | ( the_subsets_of_card ( 0 ,H)))) implies ((F | ( the_subsets_of_card ( 0 ,H))) . x) = ((F | ( the_subsets_of_card ( 0 ,H))) . y)

        proof

          let x,y be object;

          assume

           A145: x in ( dom (F | ( the_subsets_of_card ( 0 ,H))));

          

           A146: ( dom (F | ( the_subsets_of_card ( 0 ,H)))) = ( dom (F | { 0 })) by Lm2

          .= (( dom F) /\ { 0 }) by RELAT_1: 61;

          assume y in ( dom (F | ( the_subsets_of_card ( 0 ,H))));

          then y in { 0 } by A146, XBOOLE_0:def 4;

          then

           A147: y = 0 by TARSKI:def 1;

          x in { 0 } by A146, A145, XBOOLE_0:def 4;

          hence thesis by A147, TARSKI:def 1;

        end;

        hence thesis by FUNCT_1:def 10;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A143, A1);

      hence thesis;

    end;

    theorem :: RAMSEY_1:5

    ( the_subsets_of_card ( 0 ,X)) = { 0 } by Lm2;

    theorem :: RAMSEY_1:6

    

     Th6: for X be finite set st ( card X) < n holds ( the_subsets_of_card (n,X)) is empty

    proof

      let X be finite set;

      assume

       A1: ( card X) < n;

      

       A2: ( card ( Seg n)) = n by FINSEQ_1: 57;

      assume not ( the_subsets_of_card (n,X)) is empty;

      then

      consider x be object such that

       A3: x in ( the_subsets_of_card (n,X)) by XBOOLE_0:def 1;

      ex X9 be Subset of X st x = X9 & ( card X9) = n by A3;

      then ( Segm ( card ( Seg n))) c= ( Segm ( card X)) by A2, CARD_1: 11;

      then ( card ( Seg n)) <= ( card X) by NAT_1: 39;

      hence contradiction by A1, FINSEQ_1: 57;

    end;

    theorem :: RAMSEY_1:7

    X c= Y implies ( the_subsets_of_card (Z,X)) c= ( the_subsets_of_card (Z,Y)) by Lm1;

    theorem :: RAMSEY_1:8

    X is finite & Y is finite & ( card Y) = X implies ( the_subsets_of_card (X,Y)) = {Y} by Lm3;

    theorem :: RAMSEY_1:9

    X is non empty & Y is non empty implies (f is constant iff ex y be Element of Y st ( rng f) = {y}) by FUNCT_2: 111;

    theorem :: RAMSEY_1:10

    

     Th10: for X be finite set st k <= ( card X) holds ex Y be Subset of X st ( card Y) = k

    proof

      let X be finite set;

      assume k <= ( card X);

      then ( card k) <= ( card X);

      then ( Segm ( card k)) c= ( Segm ( card X)) by NAT_1: 39;

      then

      consider Y be set such that

       A1: Y c= X and

       A2: ( card Y) = ( card k) by CARD_FIL: 36;

      reconsider Y as Subset of X by A1;

      take Y;

      thus thesis by A2;

    end;

    theorem :: RAMSEY_1:11

    

     Th11: m >= 1 implies (n + 1) <= ((n + m) choose m)

    proof

      defpred Q[ Nat] means for n be Element of NAT st $1 >= 1 holds (n + 1) <= ((n + $1) choose $1);

      

       A1: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        set k9 = (k + 1);

        reconsider k9 as Element of NAT ;

        assume

         A2: Q[k];

        for n be Element of NAT st k9 >= 1 holds (n + 1) <= ((n + k9) choose k9)

        proof

          let n be Element of NAT ;

          assume

           A3: k9 >= 1;

          per cases by A3, NAT_1: 8;

            suppose

             A4: (k + 1) = 1;

            (n + 1) >= ( 0 + 1) by XREAL_1: 6;

            hence thesis by A4, NEWTON: 23;

          end;

            suppose

             A5: k >= 1;

            

             A6: ((n + k9) choose k9) = (((n + k) + 1) choose (k + 1))

            .= (((n + k) choose (k + 1)) + ((n + k) choose k)) by NEWTON: 22;

            (n + 1) <= ((n + k) choose k) by A2, A5;

            then

             A7: ((n + 1) + ((n + k) choose (k + 1))) <= ((n + k9) choose k9) by A6, XREAL_1: 6;

            ( 0 + (n + 1)) <= (((n + k) choose (k + 1)) + (n + 1)) by XREAL_1: 6;

            hence thesis by A7, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

      reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

      reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

      assume

       A8: m >= 1;

      

       A9: Q[ 0 ];

      for k be Nat holds Q[k] from NAT_1:sch 2( A9, A1);

      then (n9 + 1) <= ((n9 + m9) choose m9) by A8;

      hence thesis;

    end;

    theorem :: RAMSEY_1:12

    

     Th12: m >= 1 & n >= 1 implies (m + 1) <= ((n + m) choose m)

    proof

      defpred Q[ Nat] means for n be Element of NAT st $1 >= 1 & n >= 1 holds ($1 + 1) <= ((n + $1) choose $1);

      assume

       A1: m >= 1 & n >= 1;

      reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

      reconsider m9 = m as Element of NAT by ORDINAL1:def 12;

      

       A2: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        set k9 = (k + 1);

        reconsider k9 as Element of NAT ;

        assume

         A3: Q[k];

        for n be Element of NAT st k9 >= 1 & n >= 1 holds (k9 + 1) <= ((n + k9) choose k9)

        proof

          let n be Element of NAT ;

          assume

           A4: k9 >= 1;

          assume

           A5: n >= 1;

          per cases by A4, NAT_1: 8;

            suppose

             A6: (k + 1) = 1;

            (n + 1) >= ( 0 + 1) & (n + 1) >= (1 + 1) by A5, XREAL_1: 6;

            hence thesis by A6, NEWTON: 23;

          end;

            suppose

             A7: k >= 1;

            set k99 = (k + 1);

            

             A8: ((n + k9) choose k9) = (((n + k) + 1) choose (k + 1))

            .= (((n + k) choose (k + 1)) + ((n + k) choose k)) by NEWTON: 22;

            (k + 1) >= ( 0 + 1) by XREAL_1: 6;

            then

             A9: ((n -' 1) + 1) <= (((n -' 1) + k99) choose k99) by Th11;

            (n - 1) >= (1 - 1) by A5, XREAL_1: 9;

            then (n -' 1) = (n - 1) by XREAL_0:def 2;

            then 1 <= ((n + k) choose (k + 1)) by A5, A9, XXREAL_0: 2;

            then

             A10: (1 + (k + 1)) <= (((n + k) choose (k + 1)) + (k + 1)) by XREAL_1: 6;

            (k + 1) <= ((n + k) choose k) by A3, A5, A7;

            then ((k + 1) + ((n + k) choose (k + 1))) <= ((n + k9) choose k9) by A8, XREAL_1: 6;

            hence thesis by A10, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

      

       A11: Q[ 0 ];

      for k be Nat holds Q[k] from NAT_1:sch 2( A11, A2);

      then (m9 + 1) <= ((n9 + m9) choose m9) by A1;

      hence thesis;

    end;

    theorem :: RAMSEY_1:13

    

     Th13: for X be non empty set, p1,p2 be Element of X, P be a_partition of X, A be Element of P st p1 in A & (( proj P) . p1) = (( proj P) . p2) holds p2 in A

    proof

      let X be non empty set;

      let p1,p2 be Element of X;

      let P be a_partition of X;

      let A be Element of P;

      assume

       A1: p1 in A;

      assume (( proj P) . p1) = (( proj P) . p2);

      then

       A2: (( proj P) . p2) = A by A1, EQREL_1: 65;

      assume

       A3: not p2 in A;

      ( union P) = X by EQREL_1:def 4;

      then

      consider B be set such that

       A4: p2 in B and

       A5: B in P by TARSKI:def 4;

      reconsider B as Element of P by A5;

      

       A6: (( proj P) . p2) = B by A4, EQREL_1: 65;

      per cases by EQREL_1:def 4;

        suppose A = B;

        hence contradiction by A3, A4;

      end;

        suppose A misses B;

        then (A /\ A) = {} by A2, A6;

        hence contradiction;

      end;

    end;

    begin

    theorem :: RAMSEY_1:14

    

     Th14: for F be Function of ( the_subsets_of_card (n,X)), k st k <> 0 & X is infinite holds ex H st H is infinite & (F | ( the_subsets_of_card (n,H))) is constant

    proof

      let F be Function of ( the_subsets_of_card (n,X)), k;

      assume that

       A1: k <> 0 and

       A2: X is infinite;

      F in ( Funcs (( the_subsets_of_card (n,X)),k)) by A1, FUNCT_2: 8;

      then

       A3: ex g1 be Function st F = g1 & ( dom g1) = ( the_subsets_of_card (n,X)) & ( rng g1) c= k by FUNCT_2:def 2;

      consider Y be set such that

       A4: Y c= X and

       A5: ( card Y) = omega by A2, CARD_3: 87;

      reconsider Y as non empty set by A5;

      (Y, omega ) are_equipotent by A5, CARD_1: 5, CARD_1: 47;

      then

      consider f be Function such that

       A6: f is one-to-one and

       A7: ( dom f) = omega and

       A8: ( rng f) = Y by WELLORD2:def 4;

      reconsider f as Function of omega , Y by A7, A8, FUNCT_2: 1;

       not ( card Y) c= ( card n) by A5;

      then ( the_subsets_of_card (n,Y)) is non empty by GROUP_10: 1;

      then (f ||^ n) in ( Funcs (( the_subsets_of_card (n, omega )),( the_subsets_of_card (n,Y)))) by FUNCT_2: 8;

      then

       A9: ex g2 be Function st (f ||^ n) = g2 & ( dom g2) = ( the_subsets_of_card (n, omega )) & ( rng g2) c= ( the_subsets_of_card (n,Y)) by FUNCT_2:def 2;

      set F9 = (F * (f ||^ n));

      ( the_subsets_of_card (n,Y)) c= ( the_subsets_of_card (n,X)) by A4, Lm1;

      then

       A10: ( dom F9) = ( the_subsets_of_card (n, omega )) by A3, A9, RELAT_1: 27, XBOOLE_1: 1;

      

       A11: ( rng F9) c= ( rng F) by RELAT_1: 26;

      then

       A12: ( rng F9) c= k by A3;

      reconsider F9 as Function of ( the_subsets_of_card (n, omega )), k by A3, A10, A11, FUNCT_2: 2, XBOOLE_1: 1;

      consider H9 be Subset of omega such that

       A13: H9 is infinite and

       A14: (F9 | ( the_subsets_of_card (n,H9))) is constant by A1, Lm4, CARD_1: 47;

      

       A15: ( rng (F9 | ( the_subsets_of_card (n,H9)))) c= ( rng F9) by RELAT_1: 70;

      set H = (f .: H9);

      (f .: H9) c= ( rng f) by RELAT_1: 111;

      then

      reconsider H as Subset of X by A4, A8, XBOOLE_1: 1;

      take H;

      (H9,(f .: H9)) are_equipotent by A6, A7, CARD_1: 33;

      hence H is infinite by A13, CARD_1: 38;

      ( dom (F9 | ( the_subsets_of_card (n,H9)))) = ( the_subsets_of_card (n,H9)) by A10, Lm1, RELAT_1: 62;

      then (F9 | ( the_subsets_of_card (n,H9))) is Function of ( the_subsets_of_card (n,H9)), k by A12, A15, FUNCT_2: 2, XBOOLE_1: 1;

      then

      consider y be Element of k such that

       A16: ( rng (F9 | ( the_subsets_of_card (n,H9)))) = {y} by A1, A13, A14, FUNCT_2: 111;

      

       A17: not ( card omega ) c= ( card n);

      

       A18: ex y be Element of k st ( rng (F | ( the_subsets_of_card (n,H)))) = {y}

      proof

        take y;

        

        thus ( rng (F | ( the_subsets_of_card (n,H)))) = (F .: ( the_subsets_of_card (n,H))) by RELAT_1: 115

        .= (F .: ((f ||^ n) .: ( the_subsets_of_card (n,H9)))) by A6, A17, Th1

        .= (F9 .: ( the_subsets_of_card (n,H9))) by RELAT_1: 126

        .= {y} by A16, RELAT_1: 115;

      end;

      thus thesis by A18;

    end;

    ::$Notion-Name

    theorem :: RAMSEY_1:15

    for X be infinite set, P be a_partition of ( the_subsets_of_card (n,X)) st ( card P) = k holds ex H be Subset of X st H is infinite & H is_homogeneous_for P

    proof

      let X be infinite set;

      let P be a_partition of ( the_subsets_of_card (n,X));

      assume

       A1: ( card P) = k;

      then (P,k) are_equipotent by CARD_1:def 2;

      then

      consider F1 be Function such that

       A2: F1 is one-to-one and

       A3: ( dom F1) = P and

       A4: ( rng F1) = k by WELLORD2:def 4;

      reconsider F1 as Function of P, k by A3, A4, FUNCT_2: 1;

      set F = (F1 * ( proj P));

      reconsider F as Function of ( the_subsets_of_card (n,X)), k;

      consider H be Subset of X such that

       A5: H is infinite and

       A6: (F | ( the_subsets_of_card (n,H))) is constant by A1, Th14;

      take H;

      thus H is infinite by A5;

      set h = the Element of ( the_subsets_of_card (n,H));

      ( the_subsets_of_card (n,H)) is non empty by A5;

      then

       A7: h in ( the_subsets_of_card (n,H));

      

       A8: ( the_subsets_of_card (n,H)) c= ( the_subsets_of_card (n,X)) by Lm1;

      then

      reconsider h as Element of ( the_subsets_of_card (n,X)) by A7;

      set E = ( EqClass (h,P));

      reconsider E as Element of P by EQREL_1:def 6;

      for x be object holds x in ( the_subsets_of_card (n,H)) implies x in E

      proof

        let x be object;

        assume

         A9: x in ( the_subsets_of_card (n,H));

        then

        reconsider x9 = x as Element of ( the_subsets_of_card (n,X)) by A8;

        

         A10: ( dom F) = ( the_subsets_of_card (n,X)) by A1, FUNCT_2:def 1;

        then h in (( dom F) /\ ( the_subsets_of_card (n,H))) by A5, XBOOLE_0:def 4;

        then

         A11: h in ( dom (F | ( the_subsets_of_card (n,H)))) by RELAT_1: 61;

        x9 in (( dom F) /\ ( the_subsets_of_card (n,H))) by A9, A10, XBOOLE_0:def 4;

        then

         A12: x9 in ( dom (F | ( the_subsets_of_card (n,H)))) by RELAT_1: 61;

        (F . x9) = ((F | ( the_subsets_of_card (n,H))) . x9) by A9, FUNCT_1: 49

        .= ((F | ( the_subsets_of_card (n,H))) . h) by A6, A12, A11, FUNCT_1:def 10

        .= (F . h) by A5, FUNCT_1: 49;

        

        then (F1 . (( proj P) . x9)) = ((F1 * ( proj P)) . h) by A10, FUNCT_1: 12

        .= (F1 . (( proj P) . h)) by A10, FUNCT_1: 12;

        then h in E & (( proj P) . h) = (( proj P) . x9) by A2, A3, EQREL_1:def 6, FUNCT_1:def 4;

        hence thesis by Th13;

      end;

      then ( the_subsets_of_card (n,H)) c= E;

      hence thesis;

    end;

    begin

    scheme :: RAMSEY_1:sch1

    BinInd2 { P[ Nat, Nat] } :

P[m, n]

      provided

       A1: P[ 0 , n] & P[n, 0 ]

       and

       A2: P[(m + 1), n] & P[m, (n + 1)] implies P[(m + 1), (n + 1)];

      defpred Q[ Nat] means for m,n be Nat st (m + n) = $1 holds P[m, n];

      

       A3: for k be Nat st Q[k] holds Q[(k + 1)]

      proof

        let k be Nat;

        assume

         A4: Q[k];

        for m,n be Nat st (m + n) = (k + 1) holds P[m, n]

        proof

          let m,n be Nat;

          assume

           A5: (m + n) = (k + 1);

          per cases ;

            suppose m = 0 or n = 0 ;

            hence thesis by A1;

          end;

            suppose

             A6: m <> 0 & n <> 0 ;

            then

            reconsider m9 = (m - 1) as Element of NAT by NAT_1: 20;

            reconsider n9 = (n - 1) as Element of NAT by A6, NAT_1: 20;

            (m9 + n) = k by A5;

            then

             A7: P[m9, (n9 + 1)] by A4;

            (m + n9) = k by A5;

            then P[(m9 + 1), n9] by A4;

            hence thesis by A2, A7;

          end;

        end;

        hence thesis;

      end;

      let m, n;

      set k = (m + n);

      reconsider k as Element of NAT by ORDINAL1:def 12;

      

       A8: Q[ 0 ]

      proof

        let m,n be Nat;

        assume (m + n) = 0 ;

        then m = 0 ;

        hence thesis by A1;

      end;

      for k be Nat holds Q[k] from NAT_1:sch 2( A8, A3);

      then Q[k];

      hence thesis;

    end;

    theorem :: RAMSEY_1:16

    

     Th16: m >= 2 & n >= 2 implies ex r be Nat st r <= (((m + n) -' 2) choose (m -' 1)) & r >= 2 & for X be finite set, F be Function of ( the_subsets_of_card (2,X)), ( Seg 2) st ( card X) >= r holds ex S be Subset of X st ( card S) >= m & ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( card S) >= n & ( rng (F | ( the_subsets_of_card (2,S)))) = {2}

    proof

      defpred P[ Nat, Nat] means $1 >= 2 & $2 >= 2 implies ex r be Nat st r <= ((($1 + $2) -' 2) choose ($1 -' 1)) & r >= 2 & for X be finite set, F be Function of ( the_subsets_of_card (2,X)), ( Seg 2) st ( card X) >= r holds ex S be Subset of X st (( card S) >= $1 & ( rng (F | ( the_subsets_of_card (2,S)))) = {1}) or (( card S) >= $2 & ( rng (F | ( the_subsets_of_card (2,S)))) = {2});

      

       A1: for n,m be Nat st P[(m + 1), n] & P[m, (n + 1)] holds P[(m + 1), (n + 1)]

      proof

        let n,m be Nat;

        assume

         A2: P[(m + 1), n];

        assume

         A3: P[m, (n + 1)];

        assume that

         A4: (m + 1) >= 2 and

         A5: (n + 1) >= 2;

        per cases by XXREAL_0: 1;

          suppose (m + 1) < 2 or (n + 1) < 2;

          hence thesis by A4, A5;

        end;

          suppose

           A6: (m + 1) = 2;

          set r = (n + 1);

          take r;

          ((m + 1) + (n + 1)) >= (2 + 2) by A4, A5, XREAL_1: 7;

          then (((m + 1) + (n + 1)) - 2) >= (4 - 2) by XREAL_1: 9;

          then

           A7: (m + n) = (((m + 1) + (n + 1)) -' 2) by XREAL_0:def 2;

          ((m + 1) -' 1) = m & ((m + 1) - 1) >= (2 - 1) by A4, NAT_D: 34, XREAL_1: 9;

          hence r <= ((((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1)) by A7, Th11;

          thus r >= 2 by A5;

          let X be finite set;

          let F be Function of ( the_subsets_of_card (2,X)), ( Seg 2);

          assume

           A8: ( card X) >= r;

          F in ( Funcs (( the_subsets_of_card (2,X)),( Seg 2))) by FUNCT_2: 8;

          then

           A9: ex f be Function st F = f & ( dom f) = ( the_subsets_of_card (2,X)) & ( rng f) c= ( Seg 2) by FUNCT_2:def 2;

          per cases ;

            suppose

             A10: not 1 in ( rng F);

            consider S be Subset of X such that

             A11: ( card S) = r by A8, Th10;

            ( card 2) <= ( card S) by A5, A11;

            then ( Segm ( card 2)) c= ( Segm ( card S)) by NAT_1: 39;

            then ( the_subsets_of_card (2,S)) is non empty by A11, CARD_1: 27, GROUP_10: 1;

            then

             A12: ex x be object st x in ( the_subsets_of_card (2,S)) by XBOOLE_0:def 1;

            take S;

            

             A13: ( rng (F | ( the_subsets_of_card (2,S)))) c= ( rng F) by RELAT_1: 70;

            then

             A14: ( rng (F | ( the_subsets_of_card (2,S)))) c= {1, 2} by A9, FINSEQ_1: 2;

            ( the_subsets_of_card (2,S)) c= ( the_subsets_of_card (2,X)) by Lm1;

            then

             A15: (F | ( the_subsets_of_card (2,S))) <> {} by A9, A12;

            now

              let x be object;

              

               A16: ( rng (F | ( the_subsets_of_card (2,S)))) = {} or ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( rng (F | ( the_subsets_of_card (2,S)))) = {2} or ( rng (F | ( the_subsets_of_card (2,S)))) = {1, 2} by A14, ZFMISC_1: 36;

              hereby

                assume

                 A17: x in ( rng (F | ( the_subsets_of_card (2,S))));

                then x = 1 or x = 2 by A14, TARSKI:def 2;

                hence x = 2 by A10, A13, A17;

              end;

              assume

               A18: x = 2;

              

               A19: not 1 in ( rng (F | ( the_subsets_of_card (2,S)))) by A10, A13;

              assume not x in ( rng (F | ( the_subsets_of_card (2,S))));

              hence contradiction by A15, A18, A19, A16, TARSKI:def 1, TARSKI:def 2;

            end;

            hence thesis by A11, TARSKI:def 1;

          end;

            suppose 1 in ( rng F);

            then

            consider S be object such that

             A20: S in ( dom F) and

             A21: 1 = (F . S) by FUNCT_1:def 3;

            S in { X9 where X9 be Subset of X : ( card X9) = 2 } by A20;

            then

             A22: ex X9 be Subset of X st S = X9 & ( card X9) = 2;

            then

            reconsider S as Subset of X;

            ( the_subsets_of_card (2,S)) = {S} by A22, Lm3;

            then S in ( the_subsets_of_card (2,S)) by TARSKI:def 1;

            then

             A23: ((F | ( the_subsets_of_card (2,S))) . S) = 1 by A21, FUNCT_1: 49;

            take S;

            

             A24: {S} c= ( dom F) by A20, ZFMISC_1: 31;

            ( dom (F | ( the_subsets_of_card (2,S)))) = (( dom F) /\ ( the_subsets_of_card (2,S))) by RELAT_1: 61

            .= (( dom F) /\ {S}) by A22, Lm3

            .= {S} by A24, XBOOLE_1: 28;

            hence thesis by A6, A22, A23, FUNCT_1: 4;

          end;

        end;

          suppose

           A25: (n + 1) = 2;

          set r = (m + 1);

          take r;

          

           A26: ((n + 1) - 1) >= (2 - 1) by A5, XREAL_1: 9;

          ((m + 1) + (n + 1)) >= (2 + 2) by A4, A5, XREAL_1: 7;

          then (((m + 1) + (n + 1)) - 2) >= (4 - 2) by XREAL_1: 9;

          then

           A27: (m + n) = (((m + 1) + (n + 1)) -' 2) by XREAL_0:def 2;

          ((m + 1) -' 1) = m & ((m + 1) - 1) >= (2 - 1) by A4, NAT_D: 34, XREAL_1: 9;

          hence r <= ((((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1)) by A27, A26, Th12;

          thus r >= 2 by A4;

          let X be finite set;

          let F be Function of ( the_subsets_of_card (2,X)), ( Seg 2);

          assume

           A28: ( card X) >= r;

          F in ( Funcs (( the_subsets_of_card (2,X)),( Seg 2))) by FUNCT_2: 8;

          then

           A29: ex f be Function st F = f & ( dom f) = ( the_subsets_of_card (2,X)) & ( rng f) c= ( Seg 2) by FUNCT_2:def 2;

          per cases ;

            suppose

             A30: not 2 in ( rng F);

            consider S be Subset of X such that

             A31: ( card S) = r by A28, Th10;

            ( card 2) <= ( card S) by A4, A31;

            then ( Segm ( card 2)) c= ( Segm ( card S)) by NAT_1: 39;

            then ( the_subsets_of_card (2,S)) is non empty by A31, CARD_1: 27, GROUP_10: 1;

            then

             A32: ex x be object st x in ( the_subsets_of_card (2,S)) by XBOOLE_0:def 1;

            take S;

            

             A33: ( rng (F | ( the_subsets_of_card (2,S)))) c= ( rng F) by RELAT_1: 70;

            then

             A34: ( rng (F | ( the_subsets_of_card (2,S)))) c= {1, 2} by A29, FINSEQ_1: 2;

            ( the_subsets_of_card (2,S)) c= ( the_subsets_of_card (2,X)) by Lm1;

            then

             A35: (F | ( the_subsets_of_card (2,S))) <> {} by A29, A32;

            now

              let x be object;

              

               A36: ( rng (F | ( the_subsets_of_card (2,S)))) = {} or ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( rng (F | ( the_subsets_of_card (2,S)))) = {2} or ( rng (F | ( the_subsets_of_card (2,S)))) = {1, 2} by A34, ZFMISC_1: 36;

              hereby

                assume

                 A37: x in ( rng (F | ( the_subsets_of_card (2,S))));

                then x = 1 or x = 2 by A34, TARSKI:def 2;

                hence x = 1 by A30, A33, A37;

              end;

              assume

               A38: x = 1;

              

               A39: not 2 in ( rng (F | ( the_subsets_of_card (2,S)))) by A30, A33;

              assume not x in ( rng (F | ( the_subsets_of_card (2,S))));

              hence contradiction by A35, A38, A39, A36, TARSKI:def 1, TARSKI:def 2;

            end;

            hence thesis by A31, TARSKI:def 1;

          end;

            suppose 2 in ( rng F);

            then

            consider S be object such that

             A40: S in ( dom F) and

             A41: 2 = (F . S) by FUNCT_1:def 3;

            S in { X9 where X9 be Subset of X : ( card X9) = 2 } by A40;

            then

             A42: ex X9 be Subset of X st S = X9 & ( card X9) = 2;

            then

            reconsider S as Subset of X;

            ( the_subsets_of_card (2,S)) = {S} by A42, Lm3;

            then S in ( the_subsets_of_card (2,S)) by TARSKI:def 1;

            then

             A43: ((F | ( the_subsets_of_card (2,S))) . S) = 2 by A41, FUNCT_1: 49;

            take S;

            

             A44: {S} c= ( dom F) by A40, ZFMISC_1: 31;

            ( dom (F | ( the_subsets_of_card (2,S)))) = (( dom F) /\ ( the_subsets_of_card (2,S))) by RELAT_1: 61

            .= (( dom F) /\ {S}) by A42, Lm3

            .= {S} by A44, XBOOLE_1: 28;

            hence thesis by A25, A42, A43, FUNCT_1: 4;

          end;

        end;

          suppose

           A45: (m + 1) > 2 & (n + 1) > 2;

          set t = ((m + n) -' 1);

          set s = (m -' 1);

          ((m + 1) - 2) >= (2 - 2) by A4, XREAL_1: 9;

          then (m -' 1) = (m - 1) by XREAL_0:def 2;

          then

           A46: ((m + 1) -' 1) = (s + 1) by NAT_D: 34;

          ((m + 1) + (n + 1)) >= (2 + 2) by A4, A5, XREAL_1: 7;

          then

           A47: (((m + n) + 2) - 3) >= (4 - 3) by XREAL_1: 9;

          then

           A48: ((m + n) -' 1) = ((m + n) - 1) by XREAL_0:def 2;

          

           A49: (((m + n) + 1) -' 2) = (((m + n) + 1) - 2) by A47, XREAL_0:def 2;

          (m + n) >= 0 ;

          

          then

           A50: (((m + 1) + (n + 1)) -' 2) = (((m + 1) + (n + 1)) - 2) by XREAL_0:def 2

          .= (t + 1) by A48;

          consider r2 be Nat such that

           A51: r2 <= (((m + (n + 1)) -' 2) choose (m -' 1)) and r2 >= 2 and

           A52: for X be finite set, F be Function of ( the_subsets_of_card (2,X)), ( Seg 2) st ( card X) >= r2 holds ex S be Subset of X st ( card S) >= m & ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( card S) >= (n + 1) & ( rng (F | ( the_subsets_of_card (2,S)))) = {2} by A3, A45, NAT_1: 13;

          consider r1 be Nat such that

           A53: r1 <= ((((m + 1) + n) -' 2) choose ((m + 1) -' 1)) and

           A54: r1 >= 2 and

           A55: for X be finite set, F be Function of ( the_subsets_of_card (2,X)), ( Seg 2) st ( card X) >= r1 holds ex S be Subset of X st ( card S) >= (m + 1) & ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( card S) >= n & ( rng (F | ( the_subsets_of_card (2,S)))) = {2} by A2, A45, NAT_1: 13;

          set r = (r1 + r2);

          take r;

          (r1 + r2) <= (((((m + 1) + n) -' 2) choose ((m + 1) -' 1)) + (((m + (n + 1)) -' 2) choose (m -' 1))) by A53, A51, XREAL_1: 7;

          hence r <= ((((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1)) by A48, A49, A50, A46, NEWTON: 22;

          (r1 + r2) >= ( 0 + 2) by A54, XREAL_1: 7;

          hence r >= 2;

          let X be finite set;

          let F be Function of ( the_subsets_of_card (2,X)), ( Seg 2);

          assume ( card X) >= r;

          then

          consider S be Subset of X such that

           A56: ( card S) = r by Th10;

          consider s be object such that

           A57: s in S by A54, A56, CARD_1: 27, XBOOLE_0:def 1;

          set B = { s9 where s9 be Element of S : (F . {s, s9}) = 2 & {s, s9} in ( dom F) };

          set A = { s9 where s9 be Element of S : (F . {s, s9}) = 1 & {s, s9} in ( dom F) };

          F in ( Funcs (( the_subsets_of_card (2,X)),( Seg 2))) by FUNCT_2: 8;

          then

           A58: ex f be Function st F = f & ( dom f) = ( the_subsets_of_card (2,X)) & ( rng f) c= ( Seg 2) by FUNCT_2:def 2;

          

           A59: for x be object holds x in (A \/ B) iff x in (S \ {s})

          proof

            let x be object;

            hereby

              assume

               A60: x in (A \/ B);

              per cases by A60, XBOOLE_0:def 3;

                suppose x in A;

                then

                consider s9 be Element of S such that

                 A61: x = s9 and (F . {s, s9}) = 1 and

                 A62: {s, s9} in ( dom F);

                now

                  assume x in {s};

                  then

                   A63: x = s by TARSKI:def 1;

                   {s, s9} = ( {s} \/ {s9}) by ENUMSET1: 1

                  .= {s} by A61, A63;

                  then {s} in ( the_subsets_of_card (2,X)) by A62;

                  then ex X9 be Subset of X st X9 = {s} & ( card X9) = 2;

                  hence contradiction by CARD_1: 30;

                end;

                hence x in (S \ {s}) by A54, A56, A61, CARD_1: 27, XBOOLE_0:def 5;

              end;

                suppose x in B;

                then

                consider s9 be Element of S such that

                 A64: x = s9 and (F . {s, s9}) = 2 and

                 A65: {s, s9} in ( dom F);

                now

                  assume x in {s};

                  then

                   A66: x = s by TARSKI:def 1;

                   {s, s9} = ( {s} \/ {s9}) by ENUMSET1: 1

                  .= {s} by A64, A66;

                  then {s} in ( the_subsets_of_card (2,X)) by A65;

                  then ex X9 be Subset of X st X9 = {s} & ( card X9) = 2;

                  hence contradiction by CARD_1: 30;

                end;

                hence x in (S \ {s}) by A54, A56, A64, CARD_1: 27, XBOOLE_0:def 5;

              end;

            end;

            assume

             A67: x in (S \ {s});

            then

            reconsider s9 = x as Element of S by XBOOLE_0:def 5;

             not s9 in {s} by A67, XBOOLE_0:def 5;

            then s <> s9 by TARSKI:def 1;

            then

             A68: ( card {s, s9}) = 2 by CARD_2: 57;

             {s, s9} c= S by A57, ZFMISC_1: 32;

            then {s, s9} is Subset of X by XBOOLE_1: 1;

            then

             A69: {s, s9} in ( dom F) by A58, A68;

            then

             A70: (F . {s, s9}) in ( rng F) by FUNCT_1: 3;

            per cases by A58, A70, FINSEQ_1: 2, TARSKI:def 2;

              suppose (F . {s, s9}) = 1;

              then x in A by A69;

              hence thesis by XBOOLE_0:def 3;

            end;

              suppose (F . {s, s9}) = 2;

              then x in B by A69;

              hence thesis by XBOOLE_0:def 3;

            end;

          end;

           A71:

          now

            assume (A /\ B) <> {} ;

            then

            consider x be object such that

             A72: x in (A /\ B) by XBOOLE_0:def 1;

            x in B by A72, XBOOLE_0:def 4;

            then

             A73: ex s2 be Element of S st x = s2 & (F . {s, s2}) = 2 & {s, s2} in ( dom F);

            x in A by A72, XBOOLE_0:def 4;

            then ex s1 be Element of S st x = s1 & (F . {s, s1}) = 1 & {s, s1} in ( dom F);

            hence contradiction by A73;

          end;

          (S \ {s}) c= S by XBOOLE_1: 36;

          then

           A74: (A \/ B) c= S by A59;

           {s} c= S by A57, ZFMISC_1: 31;

          

          then

           A75: ( card (S \ {s})) = (( card S) - ( card {s})) by CARD_2: 44

          .= ((r1 + r2) - 1) by A56, CARD_1: 30;

          reconsider B as finite Subset of S by A74, XBOOLE_1: 11;

          reconsider A as finite Subset of S by A74, XBOOLE_1: 11;

          ( card (A \/ B)) = ((( card A) + ( card B)) - ( card {} )) by A71, CARD_2: 45

          .= (( card A) + ( card B));

          then

           A76: (( card A) + ( card B)) = ((r1 + r2) - 1) by A59, A75, TARSKI: 2;

          

           A77: ( card A) >= r2 or ( card B) >= r1

          proof

            assume ( card A) < r2;

            then

             A78: (( card A) + 1) <= r2 by NAT_1: 13;

            assume ( card B) < r1;

            then ((( card A) + 1) + ( card B)) < (r2 + r1) by A78, XREAL_1: 8;

            hence contradiction by A76;

          end;

          per cases by A77;

            suppose

             A79: ( card A) >= r2;

            set F9 = (F | ( the_subsets_of_card (2,A)));

            A c= X by XBOOLE_1: 1;

            then (( the_subsets_of_card (2,X)) /\ ( the_subsets_of_card (2,A))) = ( the_subsets_of_card (2,A)) by Lm1, XBOOLE_1: 28;

            then

             A80: ( dom (F | ( the_subsets_of_card (2,A)))) = ( the_subsets_of_card (2,A)) by A58, RELAT_1: 61;

            ( rng (F | ( the_subsets_of_card (2,A)))) c= ( rng F) by RELAT_1: 70;

            then

            reconsider F9 as Function of ( the_subsets_of_card (2,A)), ( Seg 2) by A58, A80, FUNCT_2: 2, XBOOLE_1: 1;

            consider S9 be Subset of A such that

             A81: ( card S9) >= m & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {1} or ( card S9) >= (n + 1) & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {2} by A52, A79;

            

             A82: (F9 | ( the_subsets_of_card (2,S9))) = (F | ( the_subsets_of_card (2,S9))) by Lm1, RELAT_1: 74;

            A c= X by XBOOLE_1: 1;

            then

            reconsider S9 as Subset of X by XBOOLE_1: 1;

            per cases by A81;

              suppose

               A83: ( card S9) >= (n + 1) & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {2};

              take S9;

              thus thesis by A83, Lm1, RELAT_1: 74;

            end;

              suppose

               A84: ( card S9) >= m & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {1};

              set S99 = (S9 \/ {s});

               {s} c= X by A57, ZFMISC_1: 31;

              then

              reconsider S99 as Subset of X by XBOOLE_1: 8;

              

               A85: ( the_subsets_of_card (2,S9)) c= ( the_subsets_of_card (2,S99)) by Lm1, XBOOLE_1: 7;

              

               A86: ( rng (F | ( the_subsets_of_card (2,S9)))) = {1} by A84, Lm1, RELAT_1: 74;

              

               A87: for y be object holds y in ( rng (F | ( the_subsets_of_card (2,S99)))) iff y = 1

              proof

                let y be object;

                (F | ( the_subsets_of_card (2,S9))) c= (F | ( the_subsets_of_card (2,S99))) by A85, RELAT_1: 75;

                then

                 A88: ( rng (F | ( the_subsets_of_card (2,S9)))) c= ( rng (F | ( the_subsets_of_card (2,S99)))) by RELAT_1: 11;

                hereby

                  assume y in ( rng (F | ( the_subsets_of_card (2,S99))));

                  then

                  consider x be object such that

                   A89: x in ( dom (F | ( the_subsets_of_card (2,S99)))) and

                   A90: y = ((F | ( the_subsets_of_card (2,S99))) . x) by FUNCT_1:def 3;

                  

                   A91: x in ( the_subsets_of_card (2,S99)) by A89, RELAT_1: 57;

                  

                   A92: x in ( dom F) by A89, RELAT_1: 57;

                  x in { S999 where S999 be Subset of S99 : ( card S999) = 2 } by A89, RELAT_1: 57;

                  then

                  consider S999 be Subset of S99 such that

                   A93: x = S999 and

                   A94: ( card S999) = 2;

                  consider s1,s2 be object such that

                   A95: s1 <> s2 and

                   A96: S999 = {s1, s2} by A94, CARD_2: 60;

                  

                   A97: s1 in S999 by A96, TARSKI:def 2;

                  

                   A98: s2 in S999 by A96, TARSKI:def 2;

                  per cases by A97, XBOOLE_0:def 3;

                    suppose

                     A99: s1 in S9;

                    per cases by A98, XBOOLE_0:def 3;

                      suppose s2 in S9;

                      then

                      reconsider x as Subset of S9 by A93, A96, A99, ZFMISC_1: 32;

                      x in ( the_subsets_of_card (2,S9)) by A93, A94;

                      then

                       A100: x in ( dom (F | ( the_subsets_of_card (2,S9)))) by A92, RELAT_1: 57;

                      then

                       A101: x in ( dom ((F | ( the_subsets_of_card (2,S99))) | ( the_subsets_of_card (2,S9)))) by A85, RELAT_1: 74;

                      ((F | ( the_subsets_of_card (2,S9))) . x) = (((F | ( the_subsets_of_card (2,S99))) | ( the_subsets_of_card (2,S9))) . x) by A85, RELAT_1: 74

                      .= ((F | ( the_subsets_of_card (2,S99))) . x) by A101, FUNCT_1: 47;

                      then y in ( rng (F | ( the_subsets_of_card (2,S9)))) by A90, A100, FUNCT_1: 3;

                      hence y = 1 by A82, A84, TARSKI:def 1;

                    end;

                      suppose

                       A102: s2 in {s};

                      s1 in A by A99;

                      then

                       A103: ex s99 be Element of S st s1 = s99 & (F . {s, s99}) = 1 & {s, s99} in ( dom F);

                      x = {s1, s} by A93, A96, A102, TARSKI:def 1;

                      hence y = 1 by A90, A91, A103, FUNCT_1: 49;

                    end;

                  end;

                    suppose

                     A104: s1 in {s};

                    then

                     A105: s <> s2 by A95, TARSKI:def 1;

                    per cases by A98, XBOOLE_0:def 3;

                      suppose s2 in S9;

                      then s2 in A;

                      then ex s99 be Element of S st s2 = s99 & (F . {s, s99}) = 1 & {s, s99} in ( dom F);

                      then (F . x) = 1 by A93, A96, A104, TARSKI:def 1;

                      hence y = 1 by A90, A91, FUNCT_1: 49;

                    end;

                      suppose s2 in {s};

                      hence y = 1 by A105, TARSKI:def 1;

                    end;

                  end;

                end;

                assume y = 1;

                then y in ( rng (F | ( the_subsets_of_card (2,S9)))) by A86, TARSKI:def 1;

                hence thesis by A88;

              end;

              take S99;

              

               A106: not s in S9

              proof

                assume s in S9;

                then s in A;

                then

                 A107: ex s9 be Element of S st s = s9 & (F . {s, s9}) = 1 & {s, s9} in ( dom F);

                 {s, s} = ( {s} \/ {s}) by ENUMSET1: 1

                .= {s};

                then {s} in ( the_subsets_of_card (2,X)) by A107;

                then ex X9 be Subset of X st X9 = {s} & ( card X9) = 2;

                hence contradiction by CARD_1: 30;

              end;

              (( card S9) + 1) >= (m + 1) by A84, XREAL_1: 6;

              hence thesis by A87, A106, CARD_2: 41, TARSKI:def 1;

            end;

          end;

            suppose

             A108: ( card B) >= r1;

            set F9 = (F | ( the_subsets_of_card (2,B)));

            B c= X by XBOOLE_1: 1;

            then (( the_subsets_of_card (2,X)) /\ ( the_subsets_of_card (2,B))) = ( the_subsets_of_card (2,B)) by Lm1, XBOOLE_1: 28;

            then

             A109: ( dom (F | ( the_subsets_of_card (2,B)))) = ( the_subsets_of_card (2,B)) by A58, RELAT_1: 61;

            ( rng (F | ( the_subsets_of_card (2,B)))) c= ( rng F) by RELAT_1: 70;

            then

            reconsider F9 as Function of ( the_subsets_of_card (2,B)), ( Seg 2) by A58, A109, FUNCT_2: 2, XBOOLE_1: 1;

            consider S9 be Subset of B such that

             A110: ( card S9) >= (m + 1) & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {1} or ( card S9) >= n & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {2} by A55, A108;

            

             A111: (F9 | ( the_subsets_of_card (2,S9))) = (F | ( the_subsets_of_card (2,S9))) by Lm1, RELAT_1: 74;

            B c= X by XBOOLE_1: 1;

            then

            reconsider S9 as Subset of X by XBOOLE_1: 1;

            per cases by A110;

              suppose

               A112: ( card S9) >= (m + 1) & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {1};

              take S9;

              thus thesis by A112, Lm1, RELAT_1: 74;

            end;

              suppose

               A113: ( card S9) >= n & ( rng (F9 | ( the_subsets_of_card (2,S9)))) = {2};

              set S99 = (S9 \/ {s});

               {s} c= X by A57, ZFMISC_1: 31;

              then

              reconsider S99 as Subset of X by XBOOLE_1: 8;

              

               A114: ( the_subsets_of_card (2,S9)) c= ( the_subsets_of_card (2,S99)) by Lm1, XBOOLE_1: 7;

              

               A115: ( rng (F | ( the_subsets_of_card (2,S9)))) = {2} by A113, Lm1, RELAT_1: 74;

              

               A116: for y be object holds y in ( rng (F | ( the_subsets_of_card (2,S99)))) iff y = 2

              proof

                let y be object;

                (F | ( the_subsets_of_card (2,S9))) c= (F | ( the_subsets_of_card (2,S99))) by A114, RELAT_1: 75;

                then

                 A117: ( rng (F | ( the_subsets_of_card (2,S9)))) c= ( rng (F | ( the_subsets_of_card (2,S99)))) by RELAT_1: 11;

                hereby

                  assume y in ( rng (F | ( the_subsets_of_card (2,S99))));

                  then

                  consider x be object such that

                   A118: x in ( dom (F | ( the_subsets_of_card (2,S99)))) and

                   A119: y = ((F | ( the_subsets_of_card (2,S99))) . x) by FUNCT_1:def 3;

                  

                   A120: x in ( the_subsets_of_card (2,S99)) by A118, RELAT_1: 57;

                  

                   A121: x in ( dom F) by A118, RELAT_1: 57;

                  x in { S999 where S999 be Subset of S99 : ( card S999) = 2 } by A118, RELAT_1: 57;

                  then

                  consider S999 be Subset of S99 such that

                   A122: x = S999 and

                   A123: ( card S999) = 2;

                  consider s1,s2 be object such that

                   A124: s1 <> s2 and

                   A125: S999 = {s1, s2} by A123, CARD_2: 60;

                  

                   A126: s1 in S999 by A125, TARSKI:def 2;

                  

                   A127: s2 in S999 by A125, TARSKI:def 2;

                  per cases by A126, XBOOLE_0:def 3;

                    suppose

                     A128: s1 in S9;

                    per cases by A127, XBOOLE_0:def 3;

                      suppose s2 in S9;

                      then

                      reconsider x as Subset of S9 by A122, A125, A128, ZFMISC_1: 32;

                      x in ( the_subsets_of_card (2,S9)) by A122, A123;

                      then

                       A129: x in ( dom (F | ( the_subsets_of_card (2,S9)))) by A121, RELAT_1: 57;

                      then

                       A130: x in ( dom ((F | ( the_subsets_of_card (2,S99))) | ( the_subsets_of_card (2,S9)))) by A114, RELAT_1: 74;

                      ((F | ( the_subsets_of_card (2,S9))) . x) = (((F | ( the_subsets_of_card (2,S99))) | ( the_subsets_of_card (2,S9))) . x) by A114, RELAT_1: 74

                      .= ((F | ( the_subsets_of_card (2,S99))) . x) by A130, FUNCT_1: 47;

                      then y in ( rng (F | ( the_subsets_of_card (2,S9)))) by A119, A129, FUNCT_1: 3;

                      hence y = 2 by A111, A113, TARSKI:def 1;

                    end;

                      suppose

                       A131: s2 in {s};

                      s1 in B by A128;

                      then

                       A132: ex s99 be Element of S st s1 = s99 & (F . {s, s99}) = 2 & {s, s99} in ( dom F);

                      x = {s1, s} by A122, A125, A131, TARSKI:def 1;

                      hence y = 2 by A119, A120, A132, FUNCT_1: 49;

                    end;

                  end;

                    suppose

                     A133: s1 in {s};

                    then

                     A134: s <> s2 by A124, TARSKI:def 1;

                    per cases by A127, XBOOLE_0:def 3;

                      suppose s2 in S9;

                      then s2 in B;

                      then ex s99 be Element of S st s2 = s99 & (F . {s, s99}) = 2 & {s, s99} in ( dom F);

                      then (F . x) = 2 by A122, A125, A133, TARSKI:def 1;

                      hence y = 2 by A119, A120, FUNCT_1: 49;

                    end;

                      suppose s2 in {s};

                      hence y = 2 by A134, TARSKI:def 1;

                    end;

                  end;

                end;

                assume y = 2;

                then y in ( rng (F | ( the_subsets_of_card (2,S9)))) by A115, TARSKI:def 1;

                hence thesis by A117;

              end;

              take S99;

              

               A135: not s in S9

              proof

                assume s in S9;

                then s in B;

                then

                 A136: ex s9 be Element of S st s = s9 & (F . {s, s9}) = 2 & {s, s9} in ( dom F);

                 {s, s} = ( {s} \/ {s}) by ENUMSET1: 1

                .= {s};

                then {s} in ( the_subsets_of_card (2,X)) by A136;

                then ex X9 be Subset of X st X9 = {s} & ( card X9) = 2;

                hence contradiction by CARD_1: 30;

              end;

              (( card S9) + 1) >= (n + 1) by A113, XREAL_1: 6;

              hence thesis by A116, A135, CARD_2: 41, TARSKI:def 1;

            end;

          end;

        end;

      end;

      

       A137: for n be Nat holds P[ 0 , n] & P[n, 0 ];

      for n,m be Nat holds P[m, n] from BinInd2( A137, A1);

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: RAMSEY_1:17

    for m be Nat holds ex r be Nat st for X be finite set, P be a_partition of ( the_subsets_of_card (2,X)) st ( card X) >= r & ( card P) = 2 holds ex S be Subset of X st ( card S) >= m & S is_homogeneous_for P

    proof

      let m be Nat;

      per cases ;

        suppose

         A1: m < 2;

        set r = 1;

        take r;

        let X be finite set;

        let P be a_partition of ( the_subsets_of_card (2,X));

        assume ( card X) >= r;

        then

        consider x be object such that

         A2: x in X by CARD_1: 27, XBOOLE_0:def 1;

        reconsider S = {x} as Subset of X by A2, ZFMISC_1: 31;

        assume ( card P) = 2;

        take S;

        m < (1 + 1) by A1;

        then m <= 1 by NAT_1: 13;

        hence ( card S) >= m by CARD_1: 30;

        

         A3: ( card S) = 1 by CARD_1: 30;

        ex p be Element of P st ( the_subsets_of_card (2,S)) c= p

        proof

          set p = the Element of P;

          take p;

          ( the_subsets_of_card (2,S)) = {} by A3, Th6;

          hence thesis;

        end;

        hence thesis;

      end;

        suppose m >= 2;

        then

        consider r be Nat such that r <= (((m + m) -' 2) choose (m -' 1)) and

         A4: r >= 2 and

         A5: for X be finite set, F be Function of ( the_subsets_of_card (2,X)), ( Seg 2) st ( card X) >= r holds ex S be Subset of X st ( card S) >= m & ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( card S) >= m & ( rng (F | ( the_subsets_of_card (2,S)))) = {2} by Th16;

        take r;

        let X be finite set;

        let P be a_partition of ( the_subsets_of_card (2,X));

        assume that

         A6: ( card X) >= r and

         A7: ( card P) = 2;

        2 <= ( card X) by A4, A6, XXREAL_0: 2;

        then ( card ( Seg 2)) <= ( card X) by FINSEQ_1: 57;

        then ( Segm ( card ( Seg 2))) c= ( Segm ( card X)) by NAT_1: 39;

        then ( card 2) c= ( card X) by FINSEQ_1: 55;

        then

        reconsider X9 = ( the_subsets_of_card (2,X)) as non empty set by A4, A6, CARD_1: 27, GROUP_10: 1;

        reconsider P9 = P as a_partition of X9;

        ( card P9) = ( card ( Seg 2)) by A7, FINSEQ_1: 57;

        then (P9,( Seg 2)) are_equipotent by CARD_1: 5;

        then

        consider F1 be Function such that

         A8: F1 is one-to-one and

         A9: ( dom F1) = P9 and

         A10: ( rng F1) = ( Seg 2) by WELLORD2:def 4;

        reconsider F1 as Function of P9, ( Seg 2) by A9, A10, FUNCT_2: 1;

        set F = (F1 * ( proj P9));

        reconsider F as Function of ( the_subsets_of_card (2,X)), ( Seg 2);

        consider S be Subset of X such that

         A11: ( card S) >= m & ( rng (F | ( the_subsets_of_card (2,S)))) = {1} or ( card S) >= m & ( rng (F | ( the_subsets_of_card (2,S)))) = {2} by A5, A6;

        take S;

        thus ( card S) >= m by A11;

        set h = the Element of ( the_subsets_of_card (2,S));

        

         A12: ( the_subsets_of_card (2,S)) is non empty by A11;

        then

         A13: h in ( the_subsets_of_card (2,S));

        

         A14: ( the_subsets_of_card (2,S)) c= ( the_subsets_of_card (2,X)) by Lm1;

        then

        reconsider h as Element of X9 by A13;

        set E = ( EqClass (h,P9));

        reconsider E as Element of P by EQREL_1:def 6;

        

         A15: (F | ( the_subsets_of_card (2,S))) is constant by A11;

        for x be object holds x in ( the_subsets_of_card (2,S)) implies x in E

        proof

          let x be object;

          assume

           A16: x in ( the_subsets_of_card (2,S));

          then

          reconsider x9 = x as Element of ( the_subsets_of_card (2,X)) by A14;

          reconsider x99 = x as Element of X9 by A14, A16;

          

           A17: ( dom F) = ( the_subsets_of_card (2,X)) by FUNCT_2:def 1;

          then h in (( dom F) /\ ( the_subsets_of_card (2,S))) by A12, XBOOLE_0:def 4;

          then

           A18: h in ( dom (F | ( the_subsets_of_card (2,S)))) by RELAT_1: 61;

          x9 in (( dom F) /\ ( the_subsets_of_card (2,S))) by A16, A17, XBOOLE_0:def 4;

          then

           A19: x9 in ( dom (F | ( the_subsets_of_card (2,S)))) by RELAT_1: 61;

          (F . x9) = ((F | ( the_subsets_of_card (2,S))) . x9) by A16, FUNCT_1: 49

          .= ((F | ( the_subsets_of_card (2,S))) . h) by A15, A19, A18, FUNCT_1:def 10

          .= (F . h) by A12, FUNCT_1: 49;

          

          then

           A20: (F1 . (( proj P9) . x9)) = ((F1 * ( proj P9)) . h) by A17, FUNCT_1: 12

          .= (F1 . (( proj P9) . h)) by A17, FUNCT_1: 12;

          (( proj P9) . x99) in P9;

          then h in E & (( proj P9) . h) = (( proj P9) . x9) by A8, A9, A20, EQREL_1:def 6, FUNCT_1:def 4;

          hence thesis by Th13;

        end;

        then ( the_subsets_of_card (2,S)) c= E;

        hence thesis;

      end;

    end;