let n, m be Nat; :: thesis: ( 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} ) ) ) ) )

defpred S1[ 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 S1[m + 1,n] & S1[m,n + 1] holds
S1[m + 1,n + 1]
proof
let n, m be Nat; :: thesis: ( S1[m + 1,n] & S1[m,n + 1] implies S1[m + 1,n + 1] )
assume A2: S1[m + 1,n] ; :: thesis: ( not S1[m,n + 1] or S1[m + 1,n + 1] )
assume A3: S1[m,n + 1] ; :: thesis: S1[m + 1,n + 1]
assume that
A4: m + 1 >= 2 and
A5: n + 1 >= 2 ; :: thesis: 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} ) ) ) )

per cases ( m + 1 < 2 or n + 1 < 2 or m + 1 = 2 or n + 1 = 2 or ( m + 1 > 2 & n + 1 > 2 ) ) by XXREAL_0:1;
suppose ( m + 1 < 2 or n + 1 < 2 ) ; :: thesis: 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} ) ) ) )

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: verum
end;
suppose A6: m + 1 = 2 ; :: thesis: 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} ) ) ) )

set r = n + 1;
take n + 1 ; :: thesis: ( n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & n + 1 >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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} ) ) ) )

(m + 1) + (n + 1) >= 2 + 2 by ;
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 ;
hence n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by ; :: thesis: ( n + 1 >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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} ) ) ) )

thus n + 1 >= 2 by A5; :: thesis: for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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} ) )

let X be finite set ; :: thesis: for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= n + 1 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} ) )

let F be Function of (the_subsets_of_card (2,X)),(Seg 2); :: thesis: ( card X >= n + 1 implies 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} ) ) )

assume A8: card X >= n + 1 ; :: thesis: 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} ) )

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 ( not 1 in rng F or 1 in rng F ) ;
suppose A10: not 1 in rng F ; :: thesis: 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} ) )

consider S being Subset of X such that
A11: card S = n + 1 by ;
card 2 <= card S by ;
then Segm (card 2) c= Segm (card S) by NAT_1:39;
then not the_subsets_of_card (2,S) is empty by ;
then A12: ex x being object st x in the_subsets_of_card (2,S) by XBOOLE_0:def 1;
take S ; :: thesis: ( ( 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} ) )
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 ;
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 ;
now :: thesis: for x being object holds
( ( x in rng (F | (the_subsets_of_card (2,S))) implies x = 2 ) & ( x = 2 implies x in rng (F | (the_subsets_of_card (2,S))) ) )
let x be object ; :: thesis: ( ( x in rng (F | (the_subsets_of_card (2,S))) implies x = 2 ) & ( x = 2 implies x in rng (F | (the_subsets_of_card (2,S))) ) )
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 ;
hereby :: thesis: ( x = 2 implies x in rng (F | (the_subsets_of_card (2,S))) )
assume A17: x in rng (F | (the_subsets_of_card (2,S))) ; :: thesis: x = 2
then ( x = 1 or x = 2 ) by ;
hence x = 2 by ; :: thesis: verum
end;
assume A18: x = 2 ; :: thesis: x in rng (F | (the_subsets_of_card (2,S)))
A19: not 1 in rng (F | (the_subsets_of_card (2,S))) by ;
assume not x in rng (F | (the_subsets_of_card (2,S))) ; :: thesis: contradiction
hence contradiction by A15, A18, A19, A16, TARSKI:def 1, TARSKI:def 2; :: thesis: verum
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 ; :: thesis: verum
end;
suppose 1 in rng F ; :: thesis: 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} ) )

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 ;
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 ;
take S ; :: thesis: ( ( 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} ) )
A24: {S} c= dom F by ;
dom (F | (the_subsets_of_card (2,S))) = (dom F) /\ (the_subsets_of_card (2,S)) by RELAT_1:61
.= (dom F) /\ {S} by
.= {S} by ;
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 ; :: thesis: verum
end;
end;
end;
suppose A25: n + 1 = 2 ; :: thesis: 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} ) ) ) )

set r = m + 1;
take m + 1 ; :: thesis: ( m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & m + 1 >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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} ) ) ) )

A26: (n + 1) - 1 >= 2 - 1 by ;
(m + 1) + (n + 1) >= 2 + 2 by ;
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 ;
hence m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by ; :: thesis: ( m + 1 >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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} ) ) ) )

thus m + 1 >= 2 by A4; :: thesis: for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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} ) )

let X be finite set ; :: thesis: for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= m + 1 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} ) )

let F be Function of (the_subsets_of_card (2,X)),(Seg 2); :: thesis: ( card X >= m + 1 implies 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} ) ) )

assume A28: card X >= m + 1 ; :: thesis: 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} ) )

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 ( not 2 in rng F or 2 in rng F ) ;
suppose A30: not 2 in rng F ; :: thesis: 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} ) )

consider S being Subset of X such that
A31: card S = m + 1 by ;
card 2 <= card S by ;
then Segm (card 2) c= Segm (card S) by NAT_1:39;
then not the_subsets_of_card (2,S) is empty by ;
then A32: ex x being object st x in the_subsets_of_card (2,S) by XBOOLE_0:def 1;
take S ; :: thesis: ( ( 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} ) )
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 ;
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 ;
now :: thesis: for x being object holds
( ( x in rng (F | (the_subsets_of_card (2,S))) implies x = 1 ) & ( x = 1 implies x in rng (F | (the_subsets_of_card (2,S))) ) )
let x be object ; :: thesis: ( ( x in rng (F | (the_subsets_of_card (2,S))) implies x = 1 ) & ( x = 1 implies x in rng (F | (the_subsets_of_card (2,S))) ) )
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 ;
hereby :: thesis: ( x = 1 implies x in rng (F | (the_subsets_of_card (2,S))) )
assume A37: x in rng (F | (the_subsets_of_card (2,S))) ; :: thesis: x = 1
then ( x = 1 or x = 2 ) by ;
hence x = 1 by ; :: thesis: verum
end;
assume A38: x = 1 ; :: thesis: x in rng (F | (the_subsets_of_card (2,S)))
A39: not 2 in rng (F | (the_subsets_of_card (2,S))) by ;
assume not x in rng (F | (the_subsets_of_card (2,S))) ; :: thesis: contradiction
hence contradiction by A35, A38, A39, A36, TARSKI:def 1, TARSKI:def 2; :: thesis: verum
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 ; :: thesis: verum
end;
suppose 2 in rng F ; :: thesis: 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} ) )

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 ;
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 ;
take S ; :: thesis: ( ( 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} ) )
A44: {S} c= dom F by ;
dom (F | (the_subsets_of_card (2,S))) = (dom F) /\ (the_subsets_of_card (2,S)) by RELAT_1:61
.= (dom F) /\ {S} by
.= {S} by ;
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 ; :: thesis: verum
end;
end;
end;
suppose A45: ( m + 1 > 2 & n + 1 > 2 ) ; :: thesis: 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} ) ) ) )

set t = (m + n) -' 1;
set s = m -' 1;
(m + 1) - 2 >= 2 - 2 by ;
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 ;
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 ;
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 ;
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 ;
set r = r1 + r2;
take r1 + r2 ; :: thesis: ( r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) & r1 + r2 >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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} ) ) ) )

r1 + r2 <= ((((m + 1) + n) -' 2) choose ((m + 1) -' 1)) + (((m + (n + 1)) -' 2) choose (m -' 1)) by ;
hence r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by ; :: thesis: ( r1 + r2 >= 2 & ( for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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} ) ) ) )

r1 + r2 >= 0 + 2 by ;
hence r1 + r2 >= 2 ; :: thesis: for X being finite set
for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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} ) )

let X be finite set ; :: thesis: for F being Function of (the_subsets_of_card (2,X)),(Seg 2) st card X >= r1 + r2 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} ) )

let F be Function of (the_subsets_of_card (2,X)),(Seg 2); :: thesis: ( card X >= r1 + r2 implies 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} ) ) )

assume card X >= r1 + r2 ; :: thesis: 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} ) )

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 ;
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: ( 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} )
hereby :: thesis: ( x in S \ {s} implies 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 ) } )
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: x in S \ {s}
per cases ( x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } or x in { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ) by ;
suppose x in { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } ; :: thesis: x in S \ {s}
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: not x in {s}
assume x in {s} ; :: thesis: contradiction
then A63: x = s by TARSKI:def 1;
{s,s9} = {s} \/ {s9} by ENUMSET1:1
.= {s} by ;
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: verum
end;
hence x in S \ {s} by ; :: thesis: verum
end;
suppose x in { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } ; :: thesis: x in S \ {s}
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: not x in {s}
assume x in {s} ; :: thesis: contradiction
then A66: x = s by TARSKI:def 1;
{s,s9} = {s} \/ {s9} by ENUMSET1:1
.= {s} by ;
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: verum
end;
hence x in S \ {s} by ; :: thesis: verum
end;
end;
end;
assume A67: x in S \ {s} ; :: thesis: 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 ) }
then reconsider s9 = x as Element of S by XBOOLE_0:def 5;
not s9 in {s} by ;
then s <> s9 by TARSKI:def 1;
then A68: card {s,s9} = 2 by CARD_2:57;
{s,s9} c= S by ;
then {s,s9} is Subset of X by XBOOLE_1:1;
then A69: {s,s9} in dom F by ;
then A70: F . {s,s9} in rng F by FUNCT_1:3;
per cases ( F . {s,s9} = 1 or F . {s,s9} = 2 ) by ;
suppose F . {s,s9} = 1 ; :: thesis: 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 ) }
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: verum
end;
suppose F . {s,s9} = 2 ; :: thesis: 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 ) }
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: verum
end;
end;
end;
A71: now :: thesis: not { 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 ) } <> {}
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: contradiction
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 ;
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 ;
then ex s1 being Element of S st
( x = s1 & F . {s,s1} = 1 & {s,s1} in dom F ) ;
hence contradiction by A73; :: thesis: verum
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 ;
then A75: card (S \ {s}) = (card S) - () by CARD_2:44
.= (r1 + r2) - 1 by ;
reconsider B = { s9 where s9 is Element of S : ( F . {s,s9} = 2 & {s,s9} in dom F ) } as finite Subset of S by ;
reconsider A = { s9 where s9 is Element of S : ( F . {s,s9} = 1 & {s,s9} in dom F ) } as finite Subset of S by ;
card (A \/ B) = ((card A) + (card B)) - () by
.= (card A) + (card B) ;
then A76: (card A) + (card B) = (r1 + r2) - 1 by ;
A77: ( card A >= r2 or card B >= r1 )
proof
assume card A < r2 ; :: thesis: card B >= r1
then A78: (card A) + 1 <= r2 by NAT_1:13;
assume card B < r1 ; :: thesis: contradiction
then ((card A) + 1) + (card B) < r2 + r1 by ;
hence contradiction by A76; :: thesis: verum
end;
per cases ( card A >= r2 or card B >= r1 ) by A77;
suppose A79: card A >= r2 ; :: thesis: 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} ) )

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 ;
then A80: dom (F | (the_subsets_of_card (2,A))) = the_subsets_of_card (2,A) by ;
rng (F | (the_subsets_of_card (2,A))) c= rng F by RELAT_1:70;
then reconsider F9 = F | (the_subsets_of_card (2,A)) as Function of (the_subsets_of_card (2,A)),(Seg 2) by ;
consider S9 being 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 ;
A82: F9 | (the_subsets_of_card (2,S9)) = F | (the_subsets_of_card (2,S9)) by ;
A c= X by XBOOLE_1:1;
then reconsider S9 = S9 as Subset of X by XBOOLE_1:1;
per cases ( ( card S9 >= n + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) or ( card S9 >= m & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) ) by A81;
suppose A83: ( card S9 >= n + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ; :: thesis: 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} ) )

take S9 ; :: thesis: ( ( 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} ) )
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 ; :: thesis: verum
end;
suppose A84: ( card S9 >= m & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) ; :: thesis: 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} ) )

set S99 = S9 \/ {s};
{s} c= X by ;
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 ;
A86: rng (F | (the_subsets_of_card (2,S9))) = {1} by ;
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: ( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 1 )
F | (the_subsets_of_card (2,S9)) c= F | (the_subsets_of_card (2,S99)) by ;
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: ( y = 1 implies y in rng (F | (the_subsets_of_card (2,S99))) )
assume y in rng (F | (the_subsets_of_card (2,S99))) ; :: thesis: y = 1
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 ;
A92: x in dom F by ;
x in { S999 where S999 is Subset of S99 : card S999 = 2 } by ;
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 ;
A97: s1 in S999 by ;
A98: s2 in S999 by ;
per cases ( s1 in S9 or s1 in {s} ) by ;
suppose A99: s1 in S9 ; :: thesis: y = 1
per cases ( s2 in S9 or s2 in {s} ) by ;
suppose s2 in S9 ; :: thesis: y = 1
then reconsider x = x as Subset of S9 by ;
x in the_subsets_of_card (2,S9) by ;
then A100: x in dom (F | (the_subsets_of_card (2,S9))) by ;
then A101: x in dom ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) by ;
(F | (the_subsets_of_card (2,S9))) . x = ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) . x by
.= (F | (the_subsets_of_card (2,S99))) . x by ;
then y in rng (F | (the_subsets_of_card (2,S9))) by ;
hence y = 1 by ; :: thesis: verum
end;
suppose A102: s2 in {s} ; :: thesis: y = 1
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 ;
hence y = 1 by ; :: thesis: verum
end;
end;
end;
suppose A104: s1 in {s} ; :: thesis: y = 1
then A105: s <> s2 by ;
per cases ( s2 in S9 or s2 in {s} ) by ;
suppose s2 in S9 ; :: thesis: y = 1
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 ;
hence y = 1 by ; :: thesis: verum
end;
suppose s2 in {s} ; :: thesis: y = 1
hence y = 1 by ; :: thesis: verum
end;
end;
end;
end;
end;
assume y = 1 ; :: thesis: y in rng (F | (the_subsets_of_card (2,S99)))
then y in rng (F | (the_subsets_of_card (2,S9))) by ;
hence y in rng (F | (the_subsets_of_card (2,S99))) by A88; :: thesis: verum
end;
take S99 ; :: thesis: ( ( 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} ) )
A106: not s in S9
proof
assume s in S9 ; :: thesis: contradiction
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: verum
end;
(card S9) + 1 >= m + 1 by ;
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 ; :: thesis: verum
end;
end;
end;
suppose A108: card B >= r1 ; :: thesis: 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} ) )

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 ;
then A109: dom (F | (the_subsets_of_card (2,B))) = the_subsets_of_card (2,B) by ;
rng (F | (the_subsets_of_card (2,B))) c= rng F by RELAT_1:70;
then reconsider F9 = F | (the_subsets_of_card (2,B)) as Function of (the_subsets_of_card (2,B)),(Seg 2) by ;
consider S9 being 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 ;
A111: F9 | (the_subsets_of_card (2,S9)) = F | (the_subsets_of_card (2,S9)) by ;
B c= X by XBOOLE_1:1;
then reconsider S9 = S9 as Subset of X by XBOOLE_1:1;
per cases ( ( 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 A110;
suppose A112: ( card S9 >= m + 1 & rng (F9 | (the_subsets_of_card (2,S9))) = {1} ) ; :: thesis: 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} ) )

take S9 ; :: thesis: ( ( 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} ) )
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 ; :: thesis: verum
end;
suppose A113: ( card S9 >= n & rng (F9 | (the_subsets_of_card (2,S9))) = {2} ) ; :: thesis: 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} ) )

set S99 = S9 \/ {s};
{s} c= X by ;
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 ;
A115: rng (F | (the_subsets_of_card (2,S9))) = {2} by ;
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: ( y in rng (F | (the_subsets_of_card (2,S99))) iff y = 2 )
F | (the_subsets_of_card (2,S9)) c= F | (the_subsets_of_card (2,S99)) by ;
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: ( y = 2 implies y in rng (F | (the_subsets_of_card (2,S99))) )
assume y in rng (F | (the_subsets_of_card (2,S99))) ; :: thesis: y = 2
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 ;
A121: x in dom F by ;
x in { S999 where S999 is Subset of S99 : card S999 = 2 } by ;
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 ;
A126: s1 in S999 by ;
A127: s2 in S999 by ;
per cases ( s1 in S9 or s1 in {s} ) by ;
suppose A128: s1 in S9 ; :: thesis: y = 2
per cases ( s2 in S9 or s2 in {s} ) by ;
suppose s2 in S9 ; :: thesis: y = 2
then reconsider x = x as Subset of S9 by ;
x in the_subsets_of_card (2,S9) by ;
then A129: x in dom (F | (the_subsets_of_card (2,S9))) by ;
then A130: x in dom ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) by ;
(F | (the_subsets_of_card (2,S9))) . x = ((F | (the_subsets_of_card (2,S99))) | (the_subsets_of_card (2,S9))) . x by
.= (F | (the_subsets_of_card (2,S99))) . x by ;
then y in rng (F | (the_subsets_of_card (2,S9))) by ;
hence y = 2 by ; :: thesis: verum
end;
suppose A131: s2 in {s} ; :: thesis: y = 2
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 ;
hence y = 2 by ; :: thesis: verum
end;
end;
end;
suppose A133: s1 in {s} ; :: thesis: y = 2
then A134: s <> s2 by ;
per cases ( s2 in S9 or s2 in {s} ) by ;
suppose s2 in S9 ; :: thesis: y = 2
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 ;
hence y = 2 by ; :: thesis: verum
end;
suppose s2 in {s} ; :: thesis: y = 2
hence y = 2 by ; :: thesis: verum
end;
end;
end;
end;
end;
assume y = 2 ; :: thesis: y in rng (F | (the_subsets_of_card (2,S99)))
then y in rng (F | (the_subsets_of_card (2,S9))) by ;
hence y in rng (F | (the_subsets_of_card (2,S99))) by A117; :: thesis: verum
end;
take S99 ; :: thesis: ( ( 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} ) )
A135: not s in S9
proof
assume s in S9 ; :: thesis: contradiction
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: verum
end;
(card S9) + 1 >= n + 1 by ;
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 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A137: for n being Nat holds
( S1[ 0 ,n] & S1[n, 0 ] ) ;
for n, m being Nat holds S1[m,n] from 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: verum