let m be natural number ; :: thesis: ex r being natural number 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 m < 2 ; :: thesis: ex r being natural number 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 m < 1 + 1 ;
then A1: m <= 1 by NAT_1:13;
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 A2: card X >= 1 ; :: thesis: ( not card P = 2 or ex S being Subset of X st
( card S >= m & S is_homogeneous_for P ) )
assume card P = 2 ; :: thesis: ex S being Subset of X st
( card S >= m & S is_homogeneous_for P )
consider x being set such that
A3: x in X by A2, CARD_1:47, XBOOLE_0:def 1;
reconsider S = {x} as Subset of X by A3, ZFMISC_1:37;
take S ; :: thesis: ( card S >= m & S is_homogeneous_for P )
A4: card S = 1 by CARD_1:50;
thus card S >= m by A1, CARD_1:50; :: thesis: S is_homogeneous_for P
ex p being Element of P st the_subsets_of_card 2,S c= p

proof

consider p being Element of P;
take p ; :: thesis: the_subsets_of_card 2,S c= p
the_subsets_of_card 2,S = {} by A4, Th6;
hence the_subsets_of_card 2,S c= p by XBOOLE_1:2; :: thesis: verum

end;

hence S is_homogeneous_for P by Def1; :: thesis: verum

end;

suppose m >= 2 ; :: thesis: ex r being natural number 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 natural number such that
A6: ( r <= ((m + m) -' 2) choose (m -' 1) & r >= 2 ) and
A7: 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 A8: ( card X >= r & card P = 2 ) ; :: thesis: ex S being Subset of X st
( card S >= m & S is_homogeneous_for P )
then 2 <= card X by A6, XXREAL_0:2;
then card (Seg 2) <= card X by FINSEQ_1:78;
then card (Seg 2) c= card X by NAT_1:40;
then A9: card 2 c= card X by FINSEQ_1:76;
reconsider X' = the_subsets_of_card 2,X as non empty set by A8, A6, A9, CARD_1:47, GROUP_10:2;
reconsider P' = P as a_partition of X' ;
card P' = card (Seg 2) by A8, FINSEQ_1:78;
then P', Seg 2 are_equipotent by CARD_1:21;
then consider F1 being Function such that
A11: ( F1 is one-to-one & dom F1 = P' & rng F1 = Seg 2 ) by WELLORD2:def 4;
reconsider F1 = F1 as Function of P',(Seg 2) by A11, FUNCT_2:3;
set F = F1 * (proj P');
reconsider F = F1 * (proj P') as Function of (the_subsets_of_card 2,X),(Seg 2) ;
consider S being Subset of X such that
A12: ( ( 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 A7, A8;
take S ; :: thesis: ( card S >= m & S is_homogeneous_for P )
thus card S >= m by A12; :: thesis: S is_homogeneous_for P
consider h being Element of the_subsets_of_card 2,S;
A13: the_subsets_of_card 2,S c= the_subsets_of_card 2,X by Lm1;
A14: not the_subsets_of_card 2,S is empty by A12;
then h in the_subsets_of_card 2,S ;
then reconsider h = h as Element of X' by A13;
A15: F | (the_subsets_of_card 2,S) is constant

proof

A16: ( 1 is Element of Seg 2 & 2 is Element of Seg 2 ) by FINSEQ_1:4, TARSKI:def 2;
F | (the_subsets_of_card 2,S) is Function of (the_subsets_of_card 2,S),(Seg 2) by A13, FUNCT_2:38;
hence F | (the_subsets_of_card 2,S) is constant by A16, A14, A12, FUNCT_2:188; :: thesis: verum

end;

set E = EqClass h,P';
reconsider E = EqClass h,P' as Element of P by EQREL_1:def 8;
for x being set st x in the_subsets_of_card 2,S holds
x in E

proof

let x be set ; :: thesis: ( x in the_subsets_of_card 2,S implies x in E )
assume A17: x in the_subsets_of_card 2,S ; :: thesis: x in E
then reconsider x' = x as Element of the_subsets_of_card 2,X by A13;
reconsider x'' = x as Element of X' by A17, A13;
A18: h in E by EQREL_1:def 8;
A19: dom F = the_subsets_of_card 2,X by FUNCT_2:def 1;
x' in (dom F) /\ (the_subsets_of_card 2,S) by A19, A17, XBOOLE_0:def 4;
then A20: x' in dom (F | (the_subsets_of_card 2,S)) by RELAT_1:90;
h in (dom F) /\ (the_subsets_of_card 2,S) by A19, A14, XBOOLE_0:def 4;
then A21: h in dom (F | (the_subsets_of_card 2,S)) by RELAT_1:90;
A22: F . x' = (F | (the_subsets_of_card 2,S)) . x' by A17, FUNCT_1:72
.= (F | (the_subsets_of_card 2,S)) . h by A15, A20, A21, FUNCT_1:def 16
.= F . h by A14, FUNCT_1:72 ;
A23: F1 . ((proj P') . x') = (F1 * (proj P')) . h by A22, A19, FUNCT_1:22
.= F1 . ((proj P') . h) by A19, FUNCT_1:22 ;
A24: (proj P') . x'' in P' ;
(proj P') . h = (proj P') . x' by A24, A23, A11, FUNCT_1:def 8;
hence x in E by A18, Th13; :: thesis: verum

end;

then the_subsets_of_card 2,S c= E by TARSKI:def 3;
hence S is_homogeneous_for P by Def1; :: thesis: verum

end;

end;