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 )

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

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 )

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

proof

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;

hence S is_homogeneous_for P ; :: thesis: verum

end;

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 )

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

proof

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;

then the_subsets_of_card (2,S) c= E ;
hence S is_homogeneous_for P ; :: thesis: verum

end;

end;