let n, m be Nat; :: thesis:
defpred S₁[ Nat, Nat] means ( $1 >= 2 & $2 >= 2 implies ex r being Nat 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, m being Nat st S₁[m + 1,n] & S₁[m,n + 1] holds
S₁[m + 1,n + 1]

let n, m be Nat; :: thesis:
assume A2: S₁[m + 1,n] ; :: thesis:
assume A3: S₁[m,n + 1] ; :: thesis:
assume that
A4: m + 1 >= 2 and
A5: n + 1 >= 2 ; :: thesis:

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

hence ex r being Nat 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 A4, A5; :: thesis:

end;

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

set r = n + 1;
take n + 1 ; :: thesis:
(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 n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A7, 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 A8: card X >= n + 1 ; :: thesis:
F in Funcs ((the_subsets_of_card (2,X)),(Seg 2)) by FUNCT_2:8;
then A9: ex f being 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 ; :: thesis:

consider S being Subset of X such that
A11: card S = n + 1 by A8, Th10;
card 2 <= card S by A5, A11;
then Segm (card 2) c= Segm (card S) by NAT_1:39;
then not the_subsets_of_card (2,S) is empty by A11, CARD_1:27, GROUP_10:1;
then A12: ex x being object st x in the_subsets_of_card (2,S) by XBOOLE_0:def 1;
take S ; :: thesis:
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 :: thesis:

let x be object ; :: thesis:
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 :: thesis:

assume A17: x in rng (F | (the_subsets_of_card (2,S))) ; :: thesis:
then ( x = 1 or x = 2 ) by A14, TARSKI:def 2;
hence x = 2 by A10, A13, A17; :: thesis:

end;

assume A18: x = 2 ; :: thesis:
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))) ; :: thesis:
hence contradiction by A15, A18, A19, A16, TARSKI:def 1, TARSKI:def 2; :: thesis:

end;

hence ( ( 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 A11, TARSKI:def 1; :: thesis:

end;

suppose 1 in rng F ; :: thesis:

then consider S being object such that
A20: S in dom F and
A21: 1 = F . S by FUNCT_1:def 3;
S in { X9 where X9 is Subset of X : card X9 = 2 } by A20;
then A22: ex X9 being Subset of X st
( S = X9 & card X9 = 2 ) ;
then reconsider S = 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 ; :: thesis:
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 ( ( 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, A22, A23, FUNCT_1:4; :: thesis:

end;

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

set r = m + 1;
take m + 1 ; :: thesis:
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 m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A27, A26, Th12; :: thesis:
thus m + 1 >= 2 by A4; :: thesis:
let X be finite set ; :: thesis:
let F be Function of (the_subsets_of_card (2,X)),(Seg 2); :: thesis:
assume A28: card X >= m + 1 ; :: thesis:
F in Funcs ((the_subsets_of_card (2,X)),(Seg 2)) by FUNCT_2:8;
then A29: ex f being 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 ; :: thesis:

consider S being Subset of X such that
A31: card S = m + 1 by A28, Th10;
card 2 <= card S by A4, A31;
then Segm (card 2) c= Segm (card S) by NAT_1:39;
then not the_subsets_of_card (2,S) is empty by A31, CARD_1:27, GROUP_10:1;
then A32: ex x being object st x in the_subsets_of_card (2,S) by XBOOLE_0:def 1;
take S ; :: thesis:
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 :: thesis:

let x be object ; :: thesis:
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 :: thesis:

assume A37: x in rng (F | (the_subsets_of_card (2,S))) ; :: thesis:
then ( x = 1 or x = 2 ) by A34, TARSKI:def 2;
hence x = 1 by A30, A33, A37; :: thesis:

end;

assume A38: x = 1 ; :: thesis:
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))) ; :: thesis:
hence contradiction by A35, A38, A39, A36, TARSKI:def 1, TARSKI:def 2; :: thesis:

end;

hence ( ( 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 A31, TARSKI:def 1; :: thesis:

end;

suppose 2 in rng F ; :: thesis:

then consider S being object such that
A40: S in dom F and
A41: 2 = F . S by FUNCT_1:def 3;
S in { X9 where X9 is Subset of X : card X9 = 2 } by A40;
then A42: ex X9 being Subset of X st
( S = X9 & card X9 = 2 ) ;
then reconsider S = 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 ; :: thesis:
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 ( ( 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 A25, A42, A43, FUNCT_1:4; :: thesis:

end;

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

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 = (m -' 1) + 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
.= ((m + n) -' 1) + 1 by A48 ;
consider r2 being Nat such that
A51: r2 <= ((m + (n + 1)) -' 2) choose (m -' 1) and
r2 >= 2 and
A52: 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 A3, A45, NAT_1:13;
consider r1 being Nat such that
A53: r1 <= (((m + 1) + n) -' 2) choose ((m + 1) -' 1) and
A54: r1 >= 2 and
A55: 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 A2, A45, NAT_1:13;
set r = r1 + r2;
take r1 + r2 ; :: thesis:
r1 + r2 <= ((((m + 1) + n) -' 2) choose ((m + 1) -' 1)) + (((m + (n + 1)) -' 2) choose (m -' 1)) by A53, A51, XREAL_1:7;
hence r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A48, A49, A50, A46, NEWTON:22; :: thesis:
r1 + r2 >= 0 + 2 by A54, XREAL_1:7;
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
A56: card S = r1 + r2 by Th10;
consider s being object such that
A57: s in S by A54, A56, CARD_1:27, XBOOLE_0:def 1;
set B = { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ;
set A = { s9 where s9 is 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 being 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 being object holds
( x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } iff x in S \ {s} )

proof

let x be object ; :: thesis:

hereby :: thesis:

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

per cases by A60, XBOOLE_0:def 3;

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

then consider s9 being Element of S such that
A61: x = s9 and
F . {s,s9} = 1 and
A62: {s,s9} in dom F ;

now :: thesis:

assume x in {s} ; :: thesis:
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 being Subset of X st
( X9 = {s} & card X9 = 2 ) ;
hence contradiction by CARD_1:30; :: thesis:

end;

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

end;

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

then consider s9 being Element of S such that
A64: x = s9 and
F . {s,s9} = 2 and
A65: {s,s9} in dom F ;

now :: thesis:

assume x in {s} ; :: thesis:
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 being Subset of X st
( X9 = {s} & card X9 = 2 ) ;
hence contradiction by CARD_1:30; :: thesis:

end;

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

end;

assume A67: x in S \ {s} ; :: thesis:
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 ; :: thesis:

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

end;

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

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

end;

A71: now :: thesis:

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

end;

S \ {s} c= S by XBOOLE_1:36;
then A74: { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } \/ { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } 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 = { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } as finite Subset of S by A74, XBOOLE_1:11;
reconsider A = { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } 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 ; :: thesis:
then A78: (card A) + 1 <= r2 by NAT_1:13;
assume card B < r1 ; :: thesis:
then ((card A) + 1) + (card B) < r2 + r1 by A78, XREAL_1:8;
hence contradiction by A76; :: thesis:

end;

per cases by A77;

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

per cases by A81;

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

take S9 ; :: thesis:
thus ( ( card S9 >= m + 1 & rng (F | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F | (the_subsets_of_card (2,S9))) = {2} ) ) by A83, Lm1, RELAT_1:74; :: thesis:

end;

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

set S99 = S9 \/ {s};
{s} c= X by A57, ZFMISC_1:31;
then reconsider S99 = S9 \/ {s} 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 being object holds
( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 1 )

proof

let y be object ; :: thesis:
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 :: thesis:

assume y in rng (F | (the_subsets_of_card (2,S99))) ; :: thesis:
then consider x being 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 is Subset of S99 : card S999 = 2 } by A89, RELAT_1:57;
then consider S999 being Subset of S99 such that
A93: x = S999 and
A94: card S999 = 2 ;
consider s1, s2 being 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 ; :: thesis:

per cases by A98, XBOOLE_0:def 3;

suppose s2 in S9 ; :: thesis:

then reconsider x = 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; :: thesis:

end;

suppose A102: s2 in {s} ; :: thesis:

s1 in A by A99;
then A103: ex s99 being 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; :: thesis:

end;

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

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

per cases by A98, XBOOLE_0:def 3;

suppose s2 in S9 ; :: thesis:

then s2 in A ;
then ex s99 being 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; :: thesis:

end;

suppose s2 in {s} ; :: thesis:

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

end;

assume y = 1 ; :: thesis:
then y in rng (F | (the_subsets_of_card (2,S9))) by A86, TARSKI:def 1;
hence y in rng (F | (the_subsets_of_card (2,S99))) by A88; :: thesis:

end;

take S99 ; :: thesis:
A106: not s in S9

proof

assume s in S9 ; :: thesis:
then s in A ;
then A107: ex s9 being 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 being Subset of X st
( X9 = {s} & card X9 = 2 ) ;
hence contradiction by CARD_1:30; :: thesis:

end;

(card S9) + 1 >= m + 1 by A84, XREAL_1:6;
hence ( ( card S99 >= m + 1 & rng (F | (the_subsets_of_card (2,S99))) = {1} ) or ( card S99 >= n + 1 & rng (F | (the_subsets_of_card (2,S99))) = {2} ) ) by A87, A106, CARD_2:41, TARSKI:def 1; :: thesis:

end;

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

per cases by A110;

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

take S9 ; :: thesis:
thus ( ( card S9 >= m + 1 & rng (F | (the_subsets_of_card (2,S9))) = {1} ) or ( card S9 >= n + 1 & rng (F | (the_subsets_of_card (2,S9))) = {2} ) ) by A112, Lm1, RELAT_1:74; :: thesis:

end;

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

set S99 = S9 \/ {s};
{s} c= X by A57, ZFMISC_1:31;
then reconsider S99 = S9 \/ {s} 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 being object holds
( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 2 )

proof

let y be object ; :: thesis:
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 :: thesis:

assume y in rng (F | (the_subsets_of_card (2,S99))) ; :: thesis:
then consider x being 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 is Subset of S99 : card S999 = 2 } by A118, RELAT_1:57;
then consider S999 being Subset of S99 such that
A122: x = S999 and
A123: card S999 = 2 ;
consider s1, s2 being 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 ; :: thesis:

per cases by A127, XBOOLE_0:def 3;

suppose s2 in S9 ; :: thesis:

end;

suppose A131: s2 in {s} ; :: thesis:

s1 in B by A128;
then A132: ex s99 being 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; :: thesis:

end;

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

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

per cases by A127, XBOOLE_0:def 3;

suppose s2 in S9 ; :: thesis:

then s2 in B ;
then ex s99 being 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; :: thesis:

end;

suppose s2 in {s} ; :: thesis:

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

end;

assume y = 2 ; :: thesis:
then y in rng (F | (the_subsets_of_card (2,S9))) by A115, TARSKI:def 1;
hence y in rng (F | (the_subsets_of_card (2,S99))) by A117; :: thesis:

end;

take S99 ; :: thesis:
A135: not s in S9

proof

assume s in S9 ; :: thesis:
then s in B ;
then A136: ex s9 being 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 being Subset of X st
( X9 = {s} & card X9 = 2 ) ;
hence contradiction by CARD_1:30; :: thesis:

end;

(card S9) + 1 >= n + 1 by A113, XREAL_1:6;
hence ( ( card S99 >= m + 1 & rng (F | (the_subsets_of_card (2,S99))) = {1} ) or ( card S99 >= n + 1 & rng (F | (the_subsets_of_card (2,S99))) = {2} ) ) by A116, A135, CARD_2:41, TARSKI:def 1; :: thesis:

end;

A137: for n being Nat holds
( S₁[ 0 ,n] & S₁[n, 0 ] ) ;
for n, m being Nat holds S₁[m,n] from RAMSEY_1:sch 1(A137, A1);
hence ( m >= 2 & n >= 2 implies ex r being Nat 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: