let m be Nat; :: thesis: ex r being Nat st

for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

per cases
( m < 2 or m >= 2 )
;

end;

suppose A1:
m < 2
; :: thesis: ex r being Nat st

for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

set r = 1;

take 1 ; :: thesis: for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= 1 & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let X be finite set ; :: thesis: for P being a_partition of the_subsets_of_card (2,X) st card X >= 1 & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let P be a_partition of the_subsets_of_card (2,X); :: thesis: ( card X >= 1 & card P = 2 implies ex S being Subset of X st

( card S >= m & S is_homogeneous_for P ) )

assume card X >= 1 ; :: thesis: ( not card P = 2 or ex S being Subset of X st

( card S >= m & S is_homogeneous_for P ) )

then consider x being object such that

A2: x in X by CARD_1:27, XBOOLE_0:def 1;

reconsider S = {x} as Subset of X by A2, ZFMISC_1:31;

assume card P = 2 ; :: thesis: ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

take S ; :: thesis: ( card S >= m & S is_homogeneous_for P )

m < 1 + 1 by A1;

then m <= 1 by NAT_1:13;

hence card S >= m by CARD_1:30; :: thesis: S is_homogeneous_for P

A3: card S = 1 by CARD_1:30;

ex p being Element of P st the_subsets_of_card (2,S) c= p

end;take 1 ; :: thesis: for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= 1 & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let X be finite set ; :: thesis: for P being a_partition of the_subsets_of_card (2,X) st card X >= 1 & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let P be a_partition of the_subsets_of_card (2,X); :: thesis: ( card X >= 1 & card P = 2 implies ex S being Subset of X st

( card S >= m & S is_homogeneous_for P ) )

assume card X >= 1 ; :: thesis: ( not card P = 2 or ex S being Subset of X st

( card S >= m & S is_homogeneous_for P ) )

then consider x being object such that

A2: x in X by CARD_1:27, XBOOLE_0:def 1;

reconsider S = {x} as Subset of X by A2, ZFMISC_1:31;

assume card P = 2 ; :: thesis: ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

take S ; :: thesis: ( card S >= m & S is_homogeneous_for P )

m < 1 + 1 by A1;

then m <= 1 by NAT_1:13;

hence card S >= m by CARD_1:30; :: thesis: S is_homogeneous_for P

A3: card S = 1 by CARD_1:30;

ex p being Element of P st the_subsets_of_card (2,S) c= p

proof

hence
S is_homogeneous_for P
; :: thesis: verum
take p = the Element of P; :: thesis: the_subsets_of_card (2,S) c= p

thus the_subsets_of_card (2,S) c= p by A3, Th6; :: thesis: verum

end;thus the_subsets_of_card (2,S) c= p by A3, Th6; :: thesis: verum

suppose
m >= 2
; :: thesis: ex r being Nat st

for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

then consider r being Nat such that

r <= ((m + m) -' 2) choose (m -' 1) and

A4: r >= 2 and

A5: 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 >= m & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by Th16;

take r ; :: thesis: for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let X be finite set ; :: thesis: for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let P be a_partition of the_subsets_of_card (2,X); :: thesis: ( card X >= r & card P = 2 implies ex S being Subset of X st

( card S >= m & S is_homogeneous_for P ) )

assume that

A6: card X >= r and

A7: card P = 2 ; :: thesis: ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

2 <= card X by A4, A6, XXREAL_0:2;

then card (Seg 2) <= card X by FINSEQ_1:57;

then Segm (card (Seg 2)) c= Segm (card X) by NAT_1:39;

then card 2 c= card X by FINSEQ_1:55;

then reconsider X9 = the_subsets_of_card (2,X) as non empty set by A4, A6, CARD_1:27, GROUP_10:1;

reconsider P9 = P as a_partition of X9 ;

card P9 = card (Seg 2) by A7, FINSEQ_1:57;

then P9, Seg 2 are_equipotent by CARD_1:5;

then consider F1 being Function such that

A8: F1 is one-to-one and

A9: dom F1 = P9 and

A10: rng F1 = Seg 2 by WELLORD2:def 4;

reconsider F1 = F1 as Function of P9,(Seg 2) by A9, A10, FUNCT_2:1;

set F = F1 * (proj P9);

reconsider F = F1 * (proj P9) as Function of (the_subsets_of_card (2,X)),(Seg 2) ;

consider S being Subset of X such that

A11: ( ( card S >= m & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= m & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by A5, A6;

take S ; :: thesis: ( card S >= m & S is_homogeneous_for P )

thus card S >= m by A11; :: thesis: S is_homogeneous_for P

set h = the Element of the_subsets_of_card (2,S);

A12: not the_subsets_of_card (2,S) is empty by A11;

then A13: the Element of the_subsets_of_card (2,S) in the_subsets_of_card (2,S) ;

A14: the_subsets_of_card (2,S) c= the_subsets_of_card (2,X) by Lm1;

then reconsider h = the Element of the_subsets_of_card (2,S) as Element of X9 by A13;

set E = EqClass (h,P9);

reconsider E = EqClass (h,P9) as Element of P by EQREL_1:def 6;

A15: F | (the_subsets_of_card (2,S)) is constant by A11;

for x being object st x in the_subsets_of_card (2,S) holds

x in E

hence S is_homogeneous_for P ; :: thesis: verum

end;r <= ((m + m) -' 2) choose (m -' 1) and

A4: r >= 2 and

A5: 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 >= m & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by Th16;

take r ; :: thesis: for X being finite set

for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let X be finite set ; :: thesis: for P being a_partition of the_subsets_of_card (2,X) st card X >= r & card P = 2 holds

ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

let P be a_partition of the_subsets_of_card (2,X); :: thesis: ( card X >= r & card P = 2 implies ex S being Subset of X st

( card S >= m & S is_homogeneous_for P ) )

assume that

A6: card X >= r and

A7: card P = 2 ; :: thesis: ex S being Subset of X st

( card S >= m & S is_homogeneous_for P )

2 <= card X by A4, A6, XXREAL_0:2;

then card (Seg 2) <= card X by FINSEQ_1:57;

then Segm (card (Seg 2)) c= Segm (card X) by NAT_1:39;

then card 2 c= card X by FINSEQ_1:55;

then reconsider X9 = the_subsets_of_card (2,X) as non empty set by A4, A6, CARD_1:27, GROUP_10:1;

reconsider P9 = P as a_partition of X9 ;

card P9 = card (Seg 2) by A7, FINSEQ_1:57;

then P9, Seg 2 are_equipotent by CARD_1:5;

then consider F1 being Function such that

A8: F1 is one-to-one and

A9: dom F1 = P9 and

A10: rng F1 = Seg 2 by WELLORD2:def 4;

reconsider F1 = F1 as Function of P9,(Seg 2) by A9, A10, FUNCT_2:1;

set F = F1 * (proj P9);

reconsider F = F1 * (proj P9) as Function of (the_subsets_of_card (2,X)),(Seg 2) ;

consider S being Subset of X such that

A11: ( ( card S >= m & rng (F | (the_subsets_of_card (2,S))) = {1} ) or ( card S >= m & rng (F | (the_subsets_of_card (2,S))) = {2} ) ) by A5, A6;

take S ; :: thesis: ( card S >= m & S is_homogeneous_for P )

thus card S >= m by A11; :: thesis: S is_homogeneous_for P

set h = the Element of the_subsets_of_card (2,S);

A12: not the_subsets_of_card (2,S) is empty by A11;

then A13: the Element of the_subsets_of_card (2,S) in the_subsets_of_card (2,S) ;

A14: the_subsets_of_card (2,S) c= the_subsets_of_card (2,X) by Lm1;

then reconsider h = the Element of the_subsets_of_card (2,S) as Element of X9 by A13;

set E = EqClass (h,P9);

reconsider E = EqClass (h,P9) as Element of P by EQREL_1:def 6;

A15: F | (the_subsets_of_card (2,S)) is constant by A11;

for x being object st x in the_subsets_of_card (2,S) holds

x in E

proof

then
the_subsets_of_card (2,S) c= E
;
let x be object ; :: thesis: ( x in the_subsets_of_card (2,S) implies x in E )

assume A16: x in the_subsets_of_card (2,S) ; :: thesis: x in E

then reconsider x9 = x as Element of the_subsets_of_card (2,X) by A14;

reconsider x99 = x as Element of X9 by A14, A16;

A17: dom F = the_subsets_of_card (2,X) by FUNCT_2:def 1;

then h in (dom F) /\ (the_subsets_of_card (2,S)) by A12, XBOOLE_0:def 4;

then A18: h in dom (F | (the_subsets_of_card (2,S))) by RELAT_1:61;

x9 in (dom F) /\ (the_subsets_of_card (2,S)) by A16, A17, XBOOLE_0:def 4;

then A19: x9 in dom (F | (the_subsets_of_card (2,S))) by RELAT_1:61;

F . x9 = (F | (the_subsets_of_card (2,S))) . x9 by A16, FUNCT_1:49

.= (F | (the_subsets_of_card (2,S))) . h by A15, A19, A18, FUNCT_1:def 10

.= F . h by A12, FUNCT_1:49 ;

then A20: F1 . ((proj P9) . x9) = (F1 * (proj P9)) . h by A17, FUNCT_1:12

.= F1 . ((proj P9) . h) by A17, FUNCT_1:12 ;

(proj P9) . x99 in P9 ;

then ( h in E & (proj P9) . h = (proj P9) . x9 ) by A8, A9, A20, EQREL_1:def 6, FUNCT_1:def 4;

hence x in E by Th13; :: thesis: verum

end;assume A16: x in the_subsets_of_card (2,S) ; :: thesis: x in E

then reconsider x9 = x as Element of the_subsets_of_card (2,X) by A14;

reconsider x99 = x as Element of X9 by A14, A16;

A17: dom F = the_subsets_of_card (2,X) by FUNCT_2:def 1;

then h in (dom F) /\ (the_subsets_of_card (2,S)) by A12, XBOOLE_0:def 4;

then A18: h in dom (F | (the_subsets_of_card (2,S))) by RELAT_1:61;

x9 in (dom F) /\ (the_subsets_of_card (2,S)) by A16, A17, XBOOLE_0:def 4;

then A19: x9 in dom (F | (the_subsets_of_card (2,S))) by RELAT_1:61;

F . x9 = (F | (the_subsets_of_card (2,S))) . x9 by A16, FUNCT_1:49

.= (F | (the_subsets_of_card (2,S))) . h by A15, A19, A18, FUNCT_1:def 10

.= F . h by A12, FUNCT_1:49 ;

then A20: F1 . ((proj P9) . x9) = (F1 * (proj P9)) . h by A17, FUNCT_1:12

.= F1 . ((proj P9) . h) by A17, FUNCT_1:12 ;

(proj P9) . x99 in P9 ;

then ( h in E & (proj P9) . h = (proj P9) . x9 ) by A8, A9, A20, EQREL_1:def 6, FUNCT_1:def 4;

hence x in E by Th13; :: thesis: verum

hence S is_homogeneous_for P ; :: thesis: verum