let m, n be natural number ; :: thesis:
defpred S₁[ natural number , natural number ] means ( $1 >= 2 & $2 >= 2 implies ex r being natural number st
( r <= (($1 + $2) -' 2) choose ($1 -' 1) & r >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card 2,X),(Seg 2) st card X >= r holds
ex S being 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 being natural number holds
( S₁[ 0 ,n] & S₁[n, 0 ] ) ;
A2: for m, n being natural number st S₁[m + 1,n] & S₁[m,n + 1] holds
S₁[m + 1,n + 1]

proof

let m, n be natural number ; :: thesis:
assume A3: S₁[m + 1,n] ; :: thesis:
assume A4: S₁[m,n + 1] ; :: thesis:
assume A5: ( m + 1 >= 2 & n + 1 >= 2 ) ; :: thesis:

per cases by XXREAL_0:1;

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

hence ex r being natural number st
( r <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card 2,X),(Seg 2) st card X >= r holds
ex S being Subset of X st
( ( card S >= m + 1 & rng (F | (the_subsets_of_card 2,S)) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card 2,S)) = {2} ) ) ) ) by A5; :: thesis:

end;

suppose A6: m + 1 = 2 ; :: thesis:

set r = n + 1;
take n + 1 ; :: thesis:
(m + 1) + (n + 1) >= 2 + 2 by A5, XREAL_1:9;
then A7: ((m + 1) + (n + 1)) - 2 >= 4 - 2 by XREAL_1:11;
A8: m + n = ((m + 1) + (n + 1)) -' 2 by A7, XREAL_0:def 2;
A9: (m + 1) -' 1 = m by NAT_D:34;
(m + 1) - 1 >= 2 - 1 by A5, XREAL_1:11;
hence n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A8, A9, Th11; :: thesis:
thus n + 1 >= 2 by A5; :: thesis:
let X be finite set ; :: thesis:
let F be Function of (the_subsets_of_card 2,X),(Seg 2); :: thesis:
assume A10: card X >= n + 1 ; :: thesis:
F in Funcs (the_subsets_of_card 2,X),(Seg 2) by FUNCT_2:11;
then consider f being Function such that
A11: ( F = f & dom f = the_subsets_of_card 2,X & rng f c= Seg 2 ) by FUNCT_2:def 2;

per cases ;

suppose A12: not 1 in rng F ; :: thesis:

consider S being Subset of X such that
A13: card S = n + 1 by A10, Th10;
A14: the_subsets_of_card 2,S c= the_subsets_of_card 2,X by Lm1;
card 2 <= card S by A5, A13, CARD_1:def 5;
then A15: card 2 c= card S by NAT_1:40;
not the_subsets_of_card 2,S is empty by A15, A13, CARD_1:47, GROUP_10:2;
then consider x being set such that
A16: x in the_subsets_of_card 2,S by XBOOLE_0:def 1;
A17: F | (the_subsets_of_card 2,S) <> {} by A11, A16, A14, RELAT_1:60, RELAT_1:86;
A18: rng (F | (the_subsets_of_card 2,S)) c= rng F by RELAT_1:99;
then A19: rng (F | (the_subsets_of_card 2,S)) c= {1,2} by A11, FINSEQ_1:4, XBOOLE_1:1;

A20: now

let x be set ; :: thesis:

hereby :: thesis:

assume A21: x in rng (F | (the_subsets_of_card 2,S)) ; :: thesis:
then ( x = 1 or x = 2 ) by A19, TARSKI:def 2;
hence x = 2 by A21, A12, A18; :: thesis:

end;

assume A22: x = 2 ; :: thesis:
assume not x in rng (F | (the_subsets_of_card 2,S)) ; :: thesis:
then A23: ( not 2 in rng (F | (the_subsets_of_card 2,S)) & not 1 in rng (F | (the_subsets_of_card 2,S)) ) by A22, A12, A18;
( 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 A19, ZFMISC_1:42;
hence contradiction by A17, A23, TARSKI:def 1, TARSKI:def 2; :: thesis:

end;

take S ; :: thesis:
thus ( ( card S >= m + 1 & rng (F | (the_subsets_of_card 2,S)) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card 2,S)) = {2} ) ) by A20, A13, TARSKI:def 1; :: thesis:

end;

suppose 1 in rng F ; :: thesis:

then consider S being set such that
A24: ( S in dom F & 1 = F . S ) by FUNCT_1:def 5;
S in { X' where X' is Subset of X : card X' = 2 } by A24;
then consider X' being Subset of X such that
A25: ( S = X' & card X' = 2 ) ;
reconsider S = S as Subset of X by A25;
A26: {S} c= dom F by A24, ZFMISC_1:37;
the_subsets_of_card 2,S = {S} by A25, Lm3;
then S in the_subsets_of_card 2,S by TARSKI:def 1;
then A27: (F | (the_subsets_of_card 2,S)) . S = 1 by A24, FUNCT_1:72;
A28: dom (F | (the_subsets_of_card 2,S)) = (dom F) /\ (the_subsets_of_card 2,S) by RELAT_1:90
.= (dom F) /\ {S} by A25, Lm3
.= {S} by A26, XBOOLE_1:28 ;
take S ; :: thesis:
thus ( ( card S >= m + 1 & rng (F | (the_subsets_of_card 2,S)) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card 2,S)) = {2} ) ) by A6, A28, A25, A27, FUNCT_1:14; :: thesis:

end;

suppose A29: n + 1 = 2 ; :: thesis:

set r = m + 1;
take m + 1 ; :: thesis:
(m + 1) + (n + 1) >= 2 + 2 by A5, XREAL_1:9;
then A30: ((m + 1) + (n + 1)) - 2 >= 4 - 2 by XREAL_1:11;
A31: m + n = ((m + 1) + (n + 1)) -' 2 by A30, XREAL_0:def 2;
A32: (m + 1) -' 1 = m by NAT_D:34;
A33: (m + 1) - 1 >= 2 - 1 by A5, XREAL_1:11;
(n + 1) - 1 >= 2 - 1 by A5, XREAL_1:11;
hence m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A31, A32, A33, Th12; :: thesis:
thus m + 1 >= 2 by A5; :: thesis:
let X be finite set ; :: thesis:
let F be Function of (the_subsets_of_card 2,X),(Seg 2); :: thesis:
assume A34: card X >= m + 1 ; :: thesis:
F in Funcs (the_subsets_of_card 2,X),(Seg 2) by FUNCT_2:11;
then consider f being Function such that
A35: ( F = f & dom f = the_subsets_of_card 2,X & rng f c= Seg 2 ) by FUNCT_2:def 2;

per cases ;

suppose A36: not 2 in rng F ; :: thesis:

consider S being Subset of X such that
A37: card S = m + 1 by A34, Th10;
A38: the_subsets_of_card 2,S c= the_subsets_of_card 2,X by Lm1;
card 2 <= card S by A5, A37, CARD_1:def 5;
then A39: card 2 c= card S by NAT_1:40;
not the_subsets_of_card 2,S is empty by A39, A37, CARD_1:47, GROUP_10:2;
then consider x being set such that
A40: x in the_subsets_of_card 2,S by XBOOLE_0:def 1;
A41: F | (the_subsets_of_card 2,S) <> {} by A35, A40, A38, RELAT_1:60, RELAT_1:86;
A42: rng (F | (the_subsets_of_card 2,S)) c= rng F by RELAT_1:99;
then A43: rng (F | (the_subsets_of_card 2,S)) c= {1,2} by A35, FINSEQ_1:4, XBOOLE_1:1;

A44: now

let x be set ; :: thesis:

hereby :: thesis:

assume A45: x in rng (F | (the_subsets_of_card 2,S)) ; :: thesis:
then ( x = 1 or x = 2 ) by A43, TARSKI:def 2;
hence x = 1 by A45, A36, A42; :: thesis:

end;

assume A46: x = 1 ; :: thesis:
assume not x in rng (F | (the_subsets_of_card 2,S)) ; :: thesis:
then A47: ( not 2 in rng (F | (the_subsets_of_card 2,S)) & not 1 in rng (F | (the_subsets_of_card 2,S)) ) by A46, A36, A42;
( 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 A43, ZFMISC_1:42;
hence contradiction by A41, A47, TARSKI:def 1, TARSKI:def 2; :: thesis:

end;

take S ; :: thesis:
thus ( ( card S >= m + 1 & rng (F | (the_subsets_of_card 2,S)) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card 2,S)) = {2} ) ) by A44, A37, TARSKI:def 1; :: thesis:

end;

suppose 2 in rng F ; :: thesis:

then consider S being set such that
A48: ( S in dom F & 2 = F . S ) by FUNCT_1:def 5;
S in { X' where X' is Subset of X : card X' = 2 } by A48;
then consider X' being Subset of X such that
A49: ( S = X' & card X' = 2 ) ;
reconsider S = S as Subset of X by A49;
A50: {S} c= dom F by A48, ZFMISC_1:37;
the_subsets_of_card 2,S = {S} by A49, Lm3;
then S in the_subsets_of_card 2,S by TARSKI:def 1;
then A51: (F | (the_subsets_of_card 2,S)) . S = 2 by A48, FUNCT_1:72;
A52: dom (F | (the_subsets_of_card 2,S)) = (dom F) /\ (the_subsets_of_card 2,S) by RELAT_1:90
.= (dom F) /\ {S} by A49, Lm3
.= {S} by A50, XBOOLE_1:28 ;
take S ; :: thesis:
thus ( ( card S >= m + 1 & rng (F | (the_subsets_of_card 2,S)) = {1} ) or ( card S >= n + 1 & rng (F | (the_subsets_of_card 2,S)) = {2} ) ) by A29, A52, A49, A51, FUNCT_1:14; :: thesis:

end;

suppose A53: ( m + 1 > 2 & n + 1 > 2 ) ; :: thesis:

consider r1 being natural number such that
A54: r1 <= (((m + 1) + n) -' 2) choose ((m + 1) -' 1) and
A55: r1 >= 2 and
A56: for X being finite set
for F being Function of (the_subsets_of_card 2,X),(Seg 2) st card X >= r1 holds
ex S being 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 A3, A53, NAT_1:13;
consider r2 being natural number such that
A57: r2 <= ((m + (n + 1)) -' 2) choose (m -' 1) and
r2 >= 2 and
A58: for X being finite set
for F being Function of (the_subsets_of_card 2,X),(Seg 2) st card X >= r2 holds
ex S being 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 A4, A53, NAT_1:13;
set r = r1 + r2;
take r1 + r2 ; :: thesis:
set s = m -' 1;
set t = (m + n) -' 1;
(m + 1) - 2 >= 2 - 2 by A5, XREAL_1:11;
then A59: m -' 1 = m - 1 by XREAL_0:def 2;
(m + 1) + (n + 1) >= 2 + 2 by A5, XREAL_1:9;
then A60: ((m + n) + 2) - 3 >= 4 - 3 by XREAL_1:11;
A61: (m + n) -' 1 = (m + n) - 1 by A60, XREAL_0:def 2;
A62: ((m + n) + 1) -' 2 = ((m + n) + 1) - 2 by A60, XREAL_0:def 2;
m + n >= 0 ;
then A63: ((m + 1) + (n + 1)) -' 2 = ((m + 1) + (n + 1)) - 2 by XREAL_0:def 2
.= ((m + n) -' 1) + 1 by A61 ;
A64: (m + 1) -' 1 = (m -' 1) + 1 by A59, NAT_D:34;
r1 + r2 <= ((((m + 1) + n) -' 2) choose ((m + 1) -' 1)) + (((m + (n + 1)) -' 2) choose (m -' 1)) by A54, A57, XREAL_1:9;
hence r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A63, A62, A61, A64, NEWTON:32; :: thesis:
r1 + r2 >= 0 + 2 by A55, XREAL_1:9;
hence r1 + r2 >= 2 ; :: thesis:
let X be finite set ; :: thesis:
let F be Function of (the_subsets_of_card 2,X),(Seg 2); :: thesis:
assume card X >= r1 + r2 ; :: thesis:
then consider S being Subset of X such that
A66: card S = r1 + r2 by Th10;
F in Funcs (the_subsets_of_card 2,X),(Seg 2) by FUNCT_2:11;
then consider f being Function such that
A67: ( F = f & dom f = the_subsets_of_card 2,X & rng f c= Seg 2 ) by FUNCT_2:def 2;
consider s being set such that
A68: s in S by A66, A55, CARD_1:47, XBOOLE_0:def 1;
set A = { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } ;
set B = { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } ;
A69: S \ {s} c= S by XBOOLE_1:36;

A70: now

assume { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } /\ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } <> {} ; :: thesis:
then consider x being set such that
A71: x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } /\ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } by XBOOLE_0:def 1;
A72: ( x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } & x in { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } ) by A71, XBOOLE_0:def 4;
then consider s1 being Element of S such that
A73: ( x = s1 & F . {s,s1} = 1 & {s,s1} in dom F ) ;
consider s2 being Element of S such that
A74: ( x = s2 & F . {s,s2} = 2 & {s,s2} in dom F ) by A72;
thus contradiction by A73, A74; :: thesis:

end;

A75: for x being set holds
( x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } \/ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } iff x in S \ {s} )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A76: x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } \/ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } ; :: thesis:

per cases by A76, XBOOLE_0:def 3;

suppose x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } ; :: thesis:

then consider s' being Element of S such that
A77: ( x = s' & F . {s,s'} = 1 & {s,s'} in dom F ) ;

now

assume x in {s} ; :: thesis:
then A78: x = s by TARSKI:def 1;
{s,s'} = {s} \/ {s'} by ENUMSET1:41
.= {s} by A77, A78 ;
then {s} in the_subsets_of_card 2,X by A77;
then consider X' being Subset of X such that
A79: ( X' = {s} & card X' = 2 ) ;
thus contradiction by A79, CARD_1:50; :: thesis:

end;

hence x in S \ {s} by A66, A55, A77, CARD_1:47, XBOOLE_0:def 5; :: thesis:

end;

suppose x in { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } ; :: thesis:

then consider s' being Element of S such that
A80: ( x = s' & F . {s,s'} = 2 & {s,s'} in dom F ) ;

now

assume x in {s} ; :: thesis:
then A81: x = s by TARSKI:def 1;
{s,s'} = {s} \/ {s'} by ENUMSET1:41
.= {s} by A80, A81 ;
then {s} in the_subsets_of_card 2,X by A80;
then consider X' being Subset of X such that
A82: ( X' = {s} & card X' = 2 ) ;
thus contradiction by A82, CARD_1:50; :: thesis:

end;

hence x in S \ {s} by A66, A55, A80, CARD_1:47, XBOOLE_0:def 5; :: thesis:

end;

assume A83: x in S \ {s} ; :: thesis:
then reconsider s' = x as Element of S by XBOOLE_0:def 5;
{s,s'} c= S by A68, ZFMISC_1:38;
then A84: {s,s'} is Subset of X by XBOOLE_1:1;
not s' in {s} by A83, XBOOLE_0:def 5;
then s <> s' by TARSKI:def 1;
then card {s,s'} = 2 by CARD_2:76;
then A85: {s,s'} in dom F by A84, A67;
then A86: F . {s,s'} in rng F by FUNCT_1:12;

per cases by A86, A67, FINSEQ_1:4, TARSKI:def 2;

suppose F . {s,s'} = 1 ; :: thesis:

then x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } by A85;
hence x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } \/ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } by XBOOLE_0:def 3; :: thesis:

end;

suppose F . {s,s'} = 2 ; :: thesis:

then x in { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } by A85;
hence x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } \/ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } by XBOOLE_0:def 3; :: thesis:

end;

A87: { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } \/ { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } c= S by A75, A69, TARSKI:2;
reconsider A = { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } as finite Subset of S by A87, XBOOLE_1:11;
reconsider B = { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } as finite Subset of S by A87, XBOOLE_1:11;
A88: card (A \/ B) = ((card A) + (card B)) - (card {} ) by A70, CARD_2:64
.= (card A) + (card B) ;
{s} c= S by A68, ZFMISC_1:37;
then card (S \ {s}) = (card S) - (card {s}) by CARD_2:63
.= (r1 + r2) - 1 by A66, CARD_1:50 ;
then A89: (card A) + (card B) = (r1 + r2) - 1 by A88, A75, TARSKI:2;
A90: ( card A >= r2 or card B >= r1 )

proof

assume card A < r2 ; :: thesis:
then A91: (card A) + 1 <= r2 by NAT_1:13;
assume card B < r1 ; :: thesis:
then ((card A) + 1) + (card B) < r2 + r1 by A91, XREAL_1:10;
hence contradiction by A89; :: thesis:

end;

per cases by A90;

suppose A92: card A >= r2 ; :: thesis:

set F' = F | (the_subsets_of_card 2,A);
A c= X by XBOOLE_1:1;
then A93: (the_subsets_of_card 2,X) /\ (the_subsets_of_card 2,A) = the_subsets_of_card 2,A by Lm1, XBOOLE_1:28;
A94: dom (F | (the_subsets_of_card 2,A)) = the_subsets_of_card 2,A by A67, A93, RELAT_1:90;
rng (F | (the_subsets_of_card 2,A)) c= rng F by RELAT_1:99;
then reconsider F' = F | (the_subsets_of_card 2,A) as Function of (the_subsets_of_card 2,A),(Seg 2) by A94, A67, FUNCT_2:4, XBOOLE_1:1;
consider S' being Subset of A such that
A95: ( ( 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 A92, A58;
A96: F' | (the_subsets_of_card 2,S') = F | (the_subsets_of_card 2,S') by Lm1, RELAT_1:103;
A c= X by XBOOLE_1:1;
then reconsider S' = S' as Subset of X by XBOOLE_1:1;

per cases by A95;

suppose A97: ( card S' >= n + 1 & rng (F' | (the_subsets_of_card 2,S')) = {2} ) ; :: thesis:

take S' ; :: thesis:
thus ( ( card S' >= m + 1 & rng (F | (the_subsets_of_card 2,S')) = {1} ) or ( card S' >= n + 1 & rng (F | (the_subsets_of_card 2,S')) = {2} ) ) by Lm1, A97, RELAT_1:103; :: thesis:

end;

suppose A98: ( card S' >= m & rng (F' | (the_subsets_of_card 2,S')) = {1} ) ; :: thesis:

set S'' = S' \/ {s};
{s} c= X by A68, ZFMISC_1:37;
then reconsider S'' = S' \/ {s} as Subset of X by XBOOLE_1:8;
A99: the_subsets_of_card 2,S' c= the_subsets_of_card 2,S'' by Lm1, XBOOLE_1:7;
A100: rng (F | (the_subsets_of_card 2,S')) = {1} by A98, Lm1, RELAT_1:103;
A101: for y being set holds
( y in rng (F | (the_subsets_of_card 2,S'')) iff y = 1 )

proof

let y be set ; :: thesis:

hereby :: thesis:

assume y in rng (F | (the_subsets_of_card 2,S'')) ; :: thesis:
then consider x being set such that
A102: x in dom (F | (the_subsets_of_card 2,S'')) and
A103: y = (F | (the_subsets_of_card 2,S'')) . x by FUNCT_1:def 5;
A104: ( x in the_subsets_of_card 2,S'' & x in dom F ) by A102, RELAT_1:86;
x in { S''' where S''' is Subset of S'' : card S''' = 2 } by A102, RELAT_1:86;
then consider S''' being Subset of S'' such that
A105: ( x = S''' & card S''' = 2 ) ;
consider s1, s2 being set such that
A106: ( s1 <> s2 & S''' = {s1,s2} ) by A105, CARD_2:79;
A107: ( s1 in S''' & s2 in S''' ) by A106, TARSKI:def 2;

per cases by A107, XBOOLE_0:def 3;

suppose A108: s1 in S' ; :: thesis:

per cases by A107, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis:

then reconsider x = x as Subset of S' by A105, A106, A108, ZFMISC_1:38;
x in the_subsets_of_card 2,S' by A105;
then A109: x in dom (F | (the_subsets_of_card 2,S')) by A104, RELAT_1:86;
A110: x in dom ((F | (the_subsets_of_card 2,S'')) | (the_subsets_of_card 2,S')) by A109, A99, RELAT_1:103;
(F | (the_subsets_of_card 2,S')) . x = ((F | (the_subsets_of_card 2,S'')) | (the_subsets_of_card 2,S')) . x by A99, RELAT_1:103
.= (F | (the_subsets_of_card 2,S'')) . x by A110, FUNCT_1:70 ;
then y in rng (F | (the_subsets_of_card 2,S')) by A103, A109, FUNCT_1:12;
hence y = 1 by A98, A96, TARSKI:def 1; :: thesis:

end;

suppose s2 in {s} ; :: thesis:

then A111: ( s1 <> s & x = {s1,s} ) by A106, A105, TARSKI:def 1;
s1 in A by A108;
then consider s'' being Element of S such that
A112: ( s1 = s'' & F . {s,s''} = 1 & {s,s''} in dom F ) ;
thus y = 1 by A103, A104, A111, A112, FUNCT_1:72; :: thesis:

end;

suppose A113: s1 in {s} ; :: thesis:

then A114: ( s <> s2 & x = {s,s2} ) by A106, A105, TARSKI:def 1;

per cases by A107, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis:

then s2 in A ;
then consider s'' being Element of S such that
A115: ( s2 = s'' & F . {s,s''} = 1 & {s,s''} in dom F ) ;
( F . x = 1 & x in dom F ) by A113, A115, A106, A105, TARSKI:def 1;
hence y = 1 by A103, A104, FUNCT_1:72; :: thesis:

end;

suppose s2 in {s} ; :: thesis:

hence y = 1 by A114, TARSKI:def 1; :: thesis:

end;

assume y = 1 ; :: thesis:
then A116: y in rng (F | (the_subsets_of_card 2,S')) by A100, TARSKI:def 1;
F | (the_subsets_of_card 2,S') c= F | (the_subsets_of_card 2,S'') by A99, RELAT_1:104;
then rng (F | (the_subsets_of_card 2,S')) c= rng (F | (the_subsets_of_card 2,S'')) by RELAT_1:25;
hence y in rng (F | (the_subsets_of_card 2,S'')) by A116; :: thesis:

end;

A117: (card S') + 1 >= m + 1 by A98, XREAL_1:8;
A118: not s in S'

proof

assume s in S' ; :: thesis:
then s in A ;
then consider s' being Element of S such that
A119: ( s = s' & F . {s,s'} = 1 & {s,s'} in dom F ) ;
A120: {s,s} = {s} \/ {s} by ENUMSET1:41
.= {s} ;
{s} in the_subsets_of_card 2,X by A119, A120;
then consider X' being Subset of X such that
A121: ( X' = {s} & card X' = 2 ) ;
thus contradiction by A121, CARD_1:50; :: thesis:

end;

take S'' ; :: thesis:
thus ( ( card S'' >= m + 1 & rng (F | (the_subsets_of_card 2,S'')) = {1} ) or ( card S'' >= n + 1 & rng (F | (the_subsets_of_card 2,S'')) = {2} ) ) by A101, A118, A117, CARD_2:54, TARSKI:def 1; :: thesis:

end;

suppose A122: card B >= r1 ; :: thesis:

set F' = F | (the_subsets_of_card 2,B);
B c= X by XBOOLE_1:1;
then A123: (the_subsets_of_card 2,X) /\ (the_subsets_of_card 2,B) = the_subsets_of_card 2,B by Lm1, XBOOLE_1:28;
A124: dom (F | (the_subsets_of_card 2,B)) = the_subsets_of_card 2,B by A67, A123, RELAT_1:90;
rng (F | (the_subsets_of_card 2,B)) c= rng F by RELAT_1:99;
then reconsider F' = F | (the_subsets_of_card 2,B) as Function of (the_subsets_of_card 2,B),(Seg 2) by A124, A67, FUNCT_2:4, XBOOLE_1:1;
consider S' being Subset of B such that
A125: ( ( 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 A122, A56;
A126: F' | (the_subsets_of_card 2,S') = F | (the_subsets_of_card 2,S') by Lm1, RELAT_1:103;
B c= X by XBOOLE_1:1;
then reconsider S' = S' as Subset of X by XBOOLE_1:1;

per cases by A125;

suppose A127: ( card S' >= m + 1 & rng (F' | (the_subsets_of_card 2,S')) = {1} ) ; :: thesis:

take S' ; :: thesis:
thus ( ( card S' >= m + 1 & rng (F | (the_subsets_of_card 2,S')) = {1} ) or ( card S' >= n + 1 & rng (F | (the_subsets_of_card 2,S')) = {2} ) ) by Lm1, A127, RELAT_1:103; :: thesis:

end;

suppose A128: ( card S' >= n & rng (F' | (the_subsets_of_card 2,S')) = {2} ) ; :: thesis:

set S'' = S' \/ {s};
{s} c= X by A68, ZFMISC_1:37;
then reconsider S'' = S' \/ {s} as Subset of X by XBOOLE_1:8;
A129: the_subsets_of_card 2,S' c= the_subsets_of_card 2,S'' by Lm1, XBOOLE_1:7;
A130: rng (F | (the_subsets_of_card 2,S')) = {2} by A128, Lm1, RELAT_1:103;
A131: for y being set holds
( y in rng (F | (the_subsets_of_card 2,S'')) iff y = 2 )

proof

let y be set ; :: thesis:

hereby :: thesis:

assume y in rng (F | (the_subsets_of_card 2,S'')) ; :: thesis:
then consider x being set such that
A132: x in dom (F | (the_subsets_of_card 2,S'')) and
A133: y = (F | (the_subsets_of_card 2,S'')) . x by FUNCT_1:def 5;
A134: ( x in the_subsets_of_card 2,S'' & x in dom F ) by A132, RELAT_1:86;
x in { S''' where S''' is Subset of S'' : card S''' = 2 } by A132, RELAT_1:86;
then consider S''' being Subset of S'' such that
A135: ( x = S''' & card S''' = 2 ) ;
consider s1, s2 being set such that
A136: ( s1 <> s2 & S''' = {s1,s2} ) by A135, CARD_2:79;
A137: ( s1 in S''' & s2 in S''' ) by A136, TARSKI:def 2;

per cases by A137, XBOOLE_0:def 3;

suppose A138: s1 in S' ; :: thesis:

per cases by A137, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis:

then reconsider x = x as Subset of S' by A135, A136, A138, ZFMISC_1:38;
x in the_subsets_of_card 2,S' by A135;
then A139: x in dom (F | (the_subsets_of_card 2,S')) by A134, RELAT_1:86;
A140: x in dom ((F | (the_subsets_of_card 2,S'')) | (the_subsets_of_card 2,S')) by A139, A129, RELAT_1:103;
(F | (the_subsets_of_card 2,S')) . x = ((F | (the_subsets_of_card 2,S'')) | (the_subsets_of_card 2,S')) . x by A129, RELAT_1:103
.= (F | (the_subsets_of_card 2,S'')) . x by A140, FUNCT_1:70 ;
then y in rng (F | (the_subsets_of_card 2,S')) by A133, A139, FUNCT_1:12;
hence y = 2 by A128, A126, TARSKI:def 1; :: thesis:

end;

suppose s2 in {s} ; :: thesis:

then A141: ( s1 <> s & x = {s1,s} ) by A136, A135, TARSKI:def 1;
s1 in B by A138;
then consider s'' being Element of S such that
A142: ( s1 = s'' & F . {s,s''} = 2 & {s,s''} in dom F ) ;
thus y = 2 by A133, A134, A141, A142, FUNCT_1:72; :: thesis:

end;

suppose A143: s1 in {s} ; :: thesis:

then A144: ( s <> s2 & x = {s,s2} ) by A136, A135, TARSKI:def 1;

per cases by A137, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis:

then s2 in B ;
then consider s'' being Element of S such that
A145: ( s2 = s'' & F . {s,s''} = 2 & {s,s''} in dom F ) ;
( F . x = 2 & x in dom F ) by A143, A145, A136, A135, TARSKI:def 1;
hence y = 2 by A133, A134, FUNCT_1:72; :: thesis:

end;

suppose s2 in {s} ; :: thesis:

hence y = 2 by A144, TARSKI:def 1; :: thesis:

end;

assume y = 2 ; :: thesis:
then A146: y in rng (F | (the_subsets_of_card 2,S')) by A130, TARSKI:def 1;
F | (the_subsets_of_card 2,S') c= F | (the_subsets_of_card 2,S'') by A129, RELAT_1:104;
then rng (F | (the_subsets_of_card 2,S')) c= rng (F | (the_subsets_of_card 2,S'')) by RELAT_1:25;
hence y in rng (F | (the_subsets_of_card 2,S'')) by A146; :: thesis:

end;

A147: (card S') + 1 >= n + 1 by A128, XREAL_1:8;
A148: not s in S'

proof

assume s in S' ; :: thesis:
then s in B ;
then consider s' being Element of S such that
A149: ( s = s' & F . {s,s'} = 2 & {s,s'} in dom F ) ;
A150: {s,s} = {s} \/ {s} by ENUMSET1:41
.= {s} ;
{s} in the_subsets_of_card 2,X by A149, A150;
then consider X' being Subset of X such that
A151: ( X' = {s} & card X' = 2 ) ;
thus contradiction by A151, CARD_1:50; :: thesis:

end;

take S'' ; :: thesis:
thus ( ( card S'' >= m + 1 & rng (F | (the_subsets_of_card 2,S'')) = {1} ) or ( card S'' >= n + 1 & rng (F | (the_subsets_of_card 2,S'')) = {2} ) ) by A131, A148, A147, CARD_2:54, TARSKI:def 1; :: thesis:

end;

for m, n being natural number holds S₁[m,n] from RAMSEY_1:sch 1(A1, A2);
hence ( m >= 2 & n >= 2 implies ex r being natural number st
( r <= ((m + n) -' 2) choose (m -' 1) & r >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card 2,X),(Seg 2) st card X >= r holds
ex S being 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} ) ) ) ) ) ; :: thesis: