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 S_{1}[ 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_{1}[m + 1,n] & S_{1}[m,n + 1] holds

S_{1}[m + 1,n + 1]

( S_{1}[ 0 ,n] & S_{1}[n, 0 ] )
;

for n, m being Nat holds S_{1}[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: verum

( 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 S

( 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

S

proof

A137:
for n being Nat holds
let n, m be Nat; :: thesis: ( S_{1}[m + 1,n] & S_{1}[m,n + 1] implies S_{1}[m + 1,n + 1] )

assume A2: S_{1}[m + 1,n]
; :: thesis: ( not S_{1}[m,n + 1] or S_{1}[m + 1,n + 1] )

assume A3: S_{1}[m,n + 1]
; :: thesis: S_{1}[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} ) ) ) )

end;assume A2: S

assume A3: S

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;

end;

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} ) ) ) )

( 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;( 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

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} ) ) ) )

( 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 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: ( 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;

end;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 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: ( 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 )
;

end;

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} ) )

( ( 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 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: ( ( 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 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;

end;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: ( ( 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 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: 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))) ) )

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( ( 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 A14, ZFMISC_1:36;

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;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: ( x = 2 implies x in rng (F | (the_subsets_of_card (2,S))) )

assume A18:
x = 2
; :: thesis: 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;then ( x = 1 or x = 2 ) by A14, TARSKI:def 2;

hence x = 2 by A10, A13, A17; :: thesis: verum

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

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} ) )

( ( 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 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: ( ( 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: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: verum

end;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: ( ( 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: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: verum

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} ) ) ) )

( 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 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: ( 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;

end;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 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: ( 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 )
;

end;

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} ) )

( ( 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 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: ( ( 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 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;

end;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: ( ( 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 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: 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))) ) )

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( ( 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 A34, ZFMISC_1:36;

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;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: ( x = 1 implies x in rng (F | (the_subsets_of_card (2,S))) )

assume A38:
x = 1
; :: thesis: 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;then ( x = 1 or x = 2 ) by A34, TARSKI:def 2;

hence x = 1 by A30, A33, A37; :: thesis: verum

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

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} ) )

( ( 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 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: ( ( 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: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: verum

end;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: ( ( 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: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: verum

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} ) ) ) )

( 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 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 + 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 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 >= 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 A54, XREAL_1:7;

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 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} )

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 )

end;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 + 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 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 >= 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 A54, XREAL_1:7;

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 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: ( 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} )

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;

end;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 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 ) } 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}

end;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 A60, XBOOLE_0:def 3;

end;

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 ;

end;A61: x = s9 and

F . {s,s9} = 1 and

A62: {s,s9} in dom F ;

now :: thesis: not x in {s}

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

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: verum

end;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: verum

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 ;

end;A64: x = s9 and

F . {s,s9} = 2 and

A65: {s,s9} in dom F ;

now :: thesis: not x in {s}

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

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: verum

end;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: verum

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
( F . {s,s9} = 1 or F . {s,s9} = 2 )
by A58, A70, FINSEQ_1:2, TARSKI:def 2;

end;

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;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

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;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

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 ) } <> {}

S \ {s} c= S
by XBOOLE_1:36;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 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: verum

end;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: verum

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: 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:8;

hence contradiction by A76; :: thesis: verum

end;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:8;

hence contradiction by A76; :: thesis: verum

per cases
( card A >= r2 or card B >= r1 )
by A77;

end;

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} ) )

( ( 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 Lm1, XBOOLE_1:28;

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

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

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

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 A52, A79;

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

A c= X by XBOOLE_1:1;

then reconsider S9 = S9 as Subset of X by XBOOLE_1:1;

end;A c= X by XBOOLE_1:1;

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

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

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

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

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 A52, A79;

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

A c= X by XBOOLE_1:1;

then reconsider S9 = 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;

end;

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} ) )

( ( 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 A83, Lm1, RELAT_1:74; :: thesis: verum

end;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: verum

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} ) )

( ( 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 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 )

A106: not s in S9

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: verum

end;{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

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} ) )
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 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;

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: verum

end;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: ( y = 1 implies y in rng (F | (the_subsets_of_card (2,S99))) )

assume
y = 1
; :: thesis: 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 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;

end;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
( s1 in S9 or s1 in {s} )
by A97, XBOOLE_0:def 3;

end;

suppose A99:
s1 in S9
; :: thesis: y = 1

end;

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

end;

suppose
s2 in S9
; :: thesis: y = 1

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: verum

end;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: verum

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

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

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

end;

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: verum

A106: not s in S9

proof

(card S9) + 1 >= m + 1
by A84, XREAL_1:6;
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;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

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: verum

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} ) )

( ( 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 Lm1, XBOOLE_1:28;

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

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

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

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 A55, A108;

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

B c= X by XBOOLE_1:1;

then reconsider S9 = S9 as Subset of X by XBOOLE_1:1;

end;B c= X by XBOOLE_1:1;

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

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

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

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

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 A55, A108;

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

B c= X by XBOOLE_1:1;

then reconsider S9 = 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;

end;

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} ) )

( ( 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 A112, Lm1, RELAT_1:74; :: thesis: verum

end;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: verum

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} ) )

( ( 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 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 )

A135: not s in S9

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: verum

end;{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

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} ) )
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 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;

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: verum

end;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: ( y = 2 implies y in rng (F | (the_subsets_of_card (2,S99))) )

assume
y = 2
; :: thesis: 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 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;

end;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
( s1 in S9 or s1 in {s} )
by A126, XBOOLE_0:def 3;

end;

suppose A128:
s1 in S9
; :: thesis: y = 2

end;

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

end;

suppose
s2 in S9
; :: thesis: y = 2

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end;

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: verum

A135: not s in S9

proof

(card S9) + 1 >= n + 1
by A113, XREAL_1:6;
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;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

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: verum

( S

for n, m being Nat holds S

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