let m, n be natural number ; :: thesis: ( 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 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 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 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 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: ( S₁[m + 1,n] & S₁[m,n + 1] implies S₁[m + 1,n + 1] )
assume A2: S₁[m + 1,n] ; :: thesis: ( not S₁[m,n + 1] or S₁[m + 1,n + 1] )
assume A3: S₁[m,n + 1] ; :: thesis: S₁[m + 1,n + 1]
assume that
A4: m + 1 >= 2 and
A5: n + 1 >= 2 ; :: thesis: 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 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 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 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 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 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 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 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 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 A4, A5, XREAL_1:9;
then ((m + 1) + (n + 1)) - 2 >= 4 - 2 by XREAL_1:11;
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:11;
hence n + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A7, Th11; :: 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 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 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 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 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 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:11;
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 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 such that
A11: card S = n + 1 by A8, Th10;
card 2 <= card S by A5, A11, CARD_1:def 5;
then card 2 c= card S by NAT_1:40;
then not the_subsets_of_card 2,S is empty by A11, CARD_1:47, GROUP_10:2;
then A12: ex x being set 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:99;
then A14: rng (F | (the_subsets_of_card 2,S)) c= {1,2} by A9, FINSEQ_1:4, XBOOLE_1:1;
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, RELAT_1:60, RELAT_1:86;

now

let x be set ; :: 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 A14, ZFMISC_1:42;

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 A14, TARSKI:def 2;
hence x = 2 by A10, A13, A17; :: 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 A10, A13;
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 A11, TARSKI:def 1; :: thesis: verum

end;

suppose 1 in rng F ; :: thesis: ex S being Subset of 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 set such that
A20: S in dom F and
A21: 1 = F . S by FUNCT_1:def 5;
S in { X' where X' is Subset of : card X' = 2 } by A20;
then A22: ex X' being Subset of st
( S = X' & card X' = 2 ) ;
then reconsider S = S as Subset of ;
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:72;
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 A20, ZFMISC_1:37;
dom (F | (the_subsets_of_card 2,S)) = (dom F) /\ (the_subsets_of_card 2,S) by RELAT_1:90
.= (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:14; :: thesis: verum

end;

end;

end;

suppose A25: n + 1 = 2 ; :: thesis: 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 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 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 A5, XREAL_1:11;
(m + 1) + (n + 1) >= 2 + 2 by A4, A5, XREAL_1:9;
then ((m + 1) + (n + 1)) - 2 >= 4 - 2 by XREAL_1:11;
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:11;
hence m + 1 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A27, A26, Th12; :: 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 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 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 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 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 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:11;
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 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 such that
A31: card S = m + 1 by A28, Th10;
card 2 <= card S by A4, A31, CARD_1:def 5;
then card 2 c= card S by NAT_1:40;
then not the_subsets_of_card 2,S is empty by A31, CARD_1:47, GROUP_10:2;
then A32: ex x being set 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:99;
then A34: rng (F | (the_subsets_of_card 2,S)) c= {1,2} by A29, FINSEQ_1:4, XBOOLE_1:1;
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, RELAT_1:60, RELAT_1:86;

now

let x be set ; :: 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 A34, ZFMISC_1:42;

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 A34, TARSKI:def 2;
hence x = 1 by A30, A33, A37; :: 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 A30, A33;
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 A31, TARSKI:def 1; :: thesis: verum

end;

suppose 2 in rng F ; :: thesis: ex S being Subset of 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 set such that
A40: S in dom F and
A41: 2 = F . S by FUNCT_1:def 5;
S in { X' where X' is Subset of : card X' = 2 } by A40;
then A42: ex X' being Subset of st
( S = X' & card X' = 2 ) ;
then reconsider S = S as Subset of ;
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:72;
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 A40, ZFMISC_1:37;
dom (F | (the_subsets_of_card 2,S)) = (dom F) /\ (the_subsets_of_card 2,S) by RELAT_1:90
.= (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:14; :: thesis: verum

end;

end;

end;

suppose A45: ( m + 1 > 2 & n + 1 > 2 ) ; :: thesis: 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 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 A4, XREAL_1:11;
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:9;
then A47: ((m + n) + 2) - 3 >= 4 - 3 by XREAL_1:11;
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 natural number 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 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 natural number 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 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 + 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 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 A53, A51, XREAL_1:9;
hence r1 + r2 <= (((m + 1) + (n + 1)) -' 2) choose ((m + 1) -' 1) by A48, A49, A50, A46, NEWTON:32; :: 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 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 A54, XREAL_1:9;
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 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 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 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 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 such that
A56: card S = r1 + r2 by Th10;
consider s being set such that
A57: s in S by A54, A56, CARD_1:47, XBOOLE_0:def 1;
set B = { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } ;
set A = { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } ;
F in Funcs (the_subsets_of_card 2,X),(Seg 2) by FUNCT_2:11;
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 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: ( 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} )

hereby :: thesis: ( x in S \ {s} implies 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 ) } )

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

per cases ( x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } or x in { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } ) by A60, XBOOLE_0:def 3;

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

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

now

assume x in {s} ; :: thesis: contradiction
then A63: x = s by TARSKI:def 1;
{s,s'} = {s} \/ {s'} by ENUMSET1:41
.= {s} by A61, A63 ;
then {s} in the_subsets_of_card 2,X by A62;
then ex X' being Subset of st
( X' = {s} & card X' = 2 ) ;
hence contradiction by CARD_1:50; :: thesis: verum

end;

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

end;

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

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

now

assume x in {s} ; :: thesis: contradiction
then A66: x = s by TARSKI:def 1;
{s,s'} = {s} \/ {s'} by ENUMSET1:41
.= {s} by A64, A66 ;
then {s} in the_subsets_of_card 2,X by A65;
then ex X' being Subset of st
( X' = {s} & card X' = 2 ) ;
hence contradiction by CARD_1:50; :: thesis: verum

end;

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

end;

end;

end;

assume A67: x in S \ {s} ; :: thesis: 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 ) }
then reconsider s' = x as Element of S by XBOOLE_0:def 5;
not s' in {s} by A67, XBOOLE_0:def 5;
then s <> s' by TARSKI:def 1;
then A68: card {s,s'} = 2 by CARD_2:76;
{s,s'} c= S by A57, ZFMISC_1:38;
then {s,s'} is Subset of by XBOOLE_1:1;
then A69: {s,s'} in dom F by A58, A68;
then A70: F . {s,s'} in rng F by FUNCT_1:12;

per cases ( F . {s,s'} = 1 or F . {s,s'} = 2 ) by A58, A70, FINSEQ_1:4, TARSKI:def 2;

suppose F . {s,s'} = 1 ; :: thesis: 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 ) }

then x in { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } by A69;
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: verum

end;

suppose F . {s,s'} = 2 ; :: thesis: 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 ) }

then x in { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } by A69;
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: verum

end;

end;

end;

A71: 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: contradiction
then consider x being set such that
A72: 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;
x in { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} 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 { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} 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: verum

end;

S \ {s} c= S by XBOOLE_1:36;
then A74: { 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 A59, TARSKI:2;
{s} c= S by A57, ZFMISC_1:37;
then A75: card (S \ {s}) = (card S) - (card {s}) by CARD_2:63
.= (r1 + r2) - 1 by A56, CARD_1:50 ;
reconsider B = { s' where s' is Element of S : ( F . {s,s'} = 2 & {s,s'} in dom F ) } as finite Subset of by A74, XBOOLE_1:11;
reconsider A = { s' where s' is Element of S : ( F . {s,s'} = 1 & {s,s'} in dom F ) } as finite Subset of by A74, XBOOLE_1:11;
card (A \/ B) = ((card A) + (card B)) - (card {} ) by A71, CARD_2:64
.= (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: 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 A78, XREAL_1:10;
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 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 F' = 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: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 A58, A80, FUNCT_2:4, XBOOLE_1:1;
consider S' being Subset of such that
A81: ( ( 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 A52, A79;
A82: 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 by XBOOLE_1:1;

per cases ( ( card S' >= n + 1 & rng (F' | (the_subsets_of_card 2,S')) = {2} ) or ( card S' >= m & rng (F' | (the_subsets_of_card 2,S')) = {1} ) ) by A81;

suppose A83: ( card S' >= n + 1 & rng (F' | (the_subsets_of_card 2,S')) = {2} ) ; :: thesis: ex S being Subset of 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 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} ) )
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 A83, Lm1, RELAT_1:103; :: thesis: verum

end;

suppose A84: ( card S' >= m & rng (F' | (the_subsets_of_card 2,S')) = {1} ) ; :: thesis: ex S being Subset of 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 S'' = S' \/ {s};
{s} c= X by A57, ZFMISC_1:37;
then reconsider S'' = S' \/ {s} as Subset of by XBOOLE_1:8;
A85: the_subsets_of_card 2,S' c= the_subsets_of_card 2,S'' by Lm1, XBOOLE_1:7;
A86: rng (F | (the_subsets_of_card 2,S')) = {1} by A84, Lm1, RELAT_1:103;
A87: for y being set holds
( y in rng (F | (the_subsets_of_card 2,S'')) iff y = 1 )

proof

let y be set ; :: thesis: ( y in rng (F | (the_subsets_of_card 2,S'')) iff y = 1 )
F | (the_subsets_of_card 2,S') c= F | (the_subsets_of_card 2,S'') by A85, RELAT_1:104;
then A88: rng (F | (the_subsets_of_card 2,S')) c= rng (F | (the_subsets_of_card 2,S'')) by RELAT_1:25;

hereby :: thesis: ( y = 1 implies y in rng (F | (the_subsets_of_card 2,S'')) )

assume y in rng (F | (the_subsets_of_card 2,S'')) ; :: thesis: y = 1
then consider x being set such that
A89: x in dom (F | (the_subsets_of_card 2,S'')) and
A90: y = (F | (the_subsets_of_card 2,S'')) . x by FUNCT_1:def 5;
A91: x in the_subsets_of_card 2,S'' by A89, RELAT_1:86;
A92: x in dom F by A89, RELAT_1:86;
x in { S''' where S''' is Subset of : card S''' = 2 } by A89, RELAT_1:86;
then consider S''' being Subset of such that
A93: x = S''' and
A94: card S''' = 2 ;
consider s1, s2 being set such that
A95: s1 <> s2 and
A96: S''' = {s1,s2} by A94, CARD_2:79;
A97: s1 in S''' by A96, TARSKI:def 2;
A98: s2 in S''' by A96, TARSKI:def 2;

per cases ( s1 in S' or s1 in {s} ) by A97, XBOOLE_0:def 3;

suppose A99: s1 in S' ; :: thesis: y = 1

per cases ( s2 in S' or s2 in {s} ) by A98, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis: y = 1

then reconsider x = x as Subset of by A93, A96, A99, ZFMISC_1:38;
x in the_subsets_of_card 2,S' by A93, A94;
then A100: x in dom (F | (the_subsets_of_card 2,S')) by A92, RELAT_1:86;
then A101: x in dom ((F | (the_subsets_of_card 2,S'')) | (the_subsets_of_card 2,S')) by A85, 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 A85, RELAT_1:103
.= (F | (the_subsets_of_card 2,S'')) . x by A101, FUNCT_1:70 ;
then y in rng (F | (the_subsets_of_card 2,S')) by A90, A100, FUNCT_1:12;
hence y = 1 by A82, A84, TARSKI:def 1; :: thesis: verum

end;

suppose A102: s2 in {s} ; :: thesis: y = 1

s1 in A by A99;
then A103: ex s'' being Element of S st
( s1 = s'' & F . {s,s''} = 1 & {s,s''} in dom F ) ;
x = {s1,s} by A93, A96, A102, TARSKI:def 1;
hence y = 1 by A90, A91, A103, FUNCT_1:72; :: thesis: verum

end;

end;

end;

suppose A104: s1 in {s} ; :: thesis: y = 1

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

per cases ( s2 in S' or s2 in {s} ) by A98, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis: y = 1

then s2 in A ;
then ex s'' being Element of S st
( s2 = s'' & F . {s,s''} = 1 & {s,s''} in dom F ) ;
then F . x = 1 by A93, A96, A104, TARSKI:def 1;
hence y = 1 by A90, A91, FUNCT_1:72; :: thesis: verum

end;

suppose s2 in {s} ; :: thesis: y = 1

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

end;

end;

end;

end;

end;

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

end;

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} ) )
A106: not s in S'

proof

assume s in S' ; :: thesis: contradiction
then s in A ;
then A107: ex s' being Element of S st
( s = s' & F . {s,s'} = 1 & {s,s'} in dom F ) ;
{s,s} = {s} \/ {s} by ENUMSET1:41
.= {s} ;
then {s} in the_subsets_of_card 2,X by A107;
then ex X' being Subset of st
( X' = {s} & card X' = 2 ) ;
hence contradiction by CARD_1:50; :: thesis: verum

end;

(card S') + 1 >= m + 1 by A84, XREAL_1:8;
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 A87, A106, CARD_2:54, TARSKI:def 1; :: thesis: verum

end;

end;

end;

suppose A108: card B >= r1 ; :: thesis: ex S being Subset of 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 F' = 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: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 A58, A109, FUNCT_2:4, XBOOLE_1:1;
consider S' being Subset of such that
A110: ( ( 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 A55, A108;
A111: 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 by XBOOLE_1:1;

per cases ( ( 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 A110;

suppose A112: ( card S' >= m + 1 & rng (F' | (the_subsets_of_card 2,S')) = {1} ) ; :: thesis: ex S being Subset of 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 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} ) )
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 A112, Lm1, RELAT_1:103; :: thesis: verum

end;

suppose A113: ( card S' >= n & rng (F' | (the_subsets_of_card 2,S')) = {2} ) ; :: thesis: ex S being Subset of 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 S'' = S' \/ {s};
{s} c= X by A57, ZFMISC_1:37;
then reconsider S'' = S' \/ {s} as Subset of by XBOOLE_1:8;
A114: the_subsets_of_card 2,S' c= the_subsets_of_card 2,S'' by Lm1, XBOOLE_1:7;
A115: rng (F | (the_subsets_of_card 2,S')) = {2} by A113, Lm1, RELAT_1:103;
A116: for y being set holds
( y in rng (F | (the_subsets_of_card 2,S'')) iff y = 2 )

proof

let y be set ; :: thesis: ( y in rng (F | (the_subsets_of_card 2,S'')) iff y = 2 )
F | (the_subsets_of_card 2,S') c= F | (the_subsets_of_card 2,S'') by A114, RELAT_1:104;
then A117: rng (F | (the_subsets_of_card 2,S')) c= rng (F | (the_subsets_of_card 2,S'')) by RELAT_1:25;

hereby :: thesis: ( y = 2 implies y in rng (F | (the_subsets_of_card 2,S'')) )

assume y in rng (F | (the_subsets_of_card 2,S'')) ; :: thesis: y = 2
then consider x being set such that
A118: x in dom (F | (the_subsets_of_card 2,S'')) and
A119: y = (F | (the_subsets_of_card 2,S'')) . x by FUNCT_1:def 5;
A120: x in the_subsets_of_card 2,S'' by A118, RELAT_1:86;
A121: x in dom F by A118, RELAT_1:86;
x in { S''' where S''' is Subset of : card S''' = 2 } by A118, RELAT_1:86;
then consider S''' being Subset of such that
A122: x = S''' and
A123: card S''' = 2 ;
consider s1, s2 being set such that
A124: s1 <> s2 and
A125: S''' = {s1,s2} by A123, CARD_2:79;
A126: s1 in S''' by A125, TARSKI:def 2;
A127: s2 in S''' by A125, TARSKI:def 2;

per cases ( s1 in S' or s1 in {s} ) by A126, XBOOLE_0:def 3;

suppose A128: s1 in S' ; :: thesis: y = 2

per cases ( s2 in S' or s2 in {s} ) by A127, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis: y = 2

then reconsider x = x as Subset of by A122, A125, A128, ZFMISC_1:38;
x in the_subsets_of_card 2,S' by A122, A123;
then A129: x in dom (F | (the_subsets_of_card 2,S')) by A121, RELAT_1:86;
then A130: x in dom ((F | (the_subsets_of_card 2,S'')) | (the_subsets_of_card 2,S')) by A114, 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 A114, RELAT_1:103
.= (F | (the_subsets_of_card 2,S'')) . x by A130, FUNCT_1:70 ;
then y in rng (F | (the_subsets_of_card 2,S')) by A119, A129, FUNCT_1:12;
hence y = 2 by A111, A113, TARSKI:def 1; :: thesis: verum

end;

suppose A131: s2 in {s} ; :: thesis: y = 2

s1 in B by A128;
then A132: ex s'' being Element of S st
( s1 = s'' & F . {s,s''} = 2 & {s,s''} in dom F ) ;
x = {s1,s} by A122, A125, A131, TARSKI:def 1;
hence y = 2 by A119, A120, A132, FUNCT_1:72; :: thesis: verum

end;

end;

end;

suppose A133: s1 in {s} ; :: thesis: y = 2

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

per cases ( s2 in S' or s2 in {s} ) by A127, XBOOLE_0:def 3;

suppose s2 in S' ; :: thesis: y = 2

then s2 in B ;
then ex s'' being Element of S st
( s2 = s'' & F . {s,s''} = 2 & {s,s''} in dom F ) ;
then F . x = 2 by A122, A125, A133, TARSKI:def 1;
hence y = 2 by A119, A120, FUNCT_1:72; :: thesis: verum

end;

suppose s2 in {s} ; :: thesis: y = 2

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

end;

end;

end;

end;

end;

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

end;

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} ) )
A135: not s in S'

proof

assume s in S' ; :: thesis: contradiction
then s in B ;
then A136: ex s' being Element of S st
( s = s' & F . {s,s'} = 2 & {s,s'} in dom F ) ;
{s,s} = {s} \/ {s} by ENUMSET1:41
.= {s} ;
then {s} in the_subsets_of_card 2,X by A136;
then ex X' being Subset of st
( X' = {s} & card X' = 2 ) ;
hence contradiction by CARD_1:50; :: thesis: verum

end;

(card S') + 1 >= n + 1 by A113, XREAL_1:8;
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 A116, A135, CARD_2:54, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A137: for n being natural number holds
( S₁[ 0 ,n] & S₁[n, 0 ] ) ;
for m, n being natural number holds S₁[m,n] from RAMSEY_1:sch 1(A137, A1);
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 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