let m be natural number ; :: thesis:

suppose A1: m < 2 ; :: thesis:

set r = 1;
take 1 ; :: thesis:
let X be finite set ; :: thesis:
let P be a_partition of the_subsets_of_card 2,X; :: thesis:
assume card X >= 1 ; :: thesis:
then consider x being set such that
A2: x in X by CARD_1:47, XBOOLE_0:def 1;
reconsider S = {x} as Subset of by A2, ZFMISC_1:37;
assume card P = 2 ; :: thesis:
take S ; :: thesis:
m < 1 + 1 by A1;
then m <= 1 by NAT_1:13;
hence card S >= m by CARD_1:50; :: thesis:
A3: card S = 1 by CARD_1:50;
ex p being Element of P st the_subsets_of_card 2,S c= p

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

end;

hence S is_homogeneous_for P by Def1; :: thesis:

end;

suppose m >= 2 ; :: thesis:

then consider r being natural number 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 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:
let X be finite set ; :: thesis:
let P be a_partition of the_subsets_of_card 2,X; :: thesis:
assume that
A6: card X >= r and
A7: card P = 2 ; :: thesis:
2 <= card X by A4, 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 card 2 c= card X by FINSEQ_1:76;
then reconsider X' = the_subsets_of_card 2,X as non empty set by A4, A6, CARD_1:47, GROUP_10:2;
reconsider P' = P as a_partition of X' ;
card P' = card (Seg 2) by A7, FINSEQ_1:78;
then P', Seg 2 are_equipotent by CARD_1:21;
then consider F1 being Function such that
A8: F1 is one-to-one and
A9: dom F1 = P' and
A10: rng F1 = Seg 2 by WELLORD2:def 4;
reconsider F1 = F1 as Function of P', Seg 2 by A9, A10, 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 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:
thus card S >= m by A11; :: thesis:
consider h being Element of the_subsets_of_card 2,S;
A12: not the_subsets_of_card 2,S is empty by A11;
then A13: h in the_subsets_of_card 2,S ;
A14: ( 1 is Element of Seg 2 & 2 is Element of Seg 2 ) by FINSEQ_1:4, TARSKI:def 2;
A15: the_subsets_of_card 2,S c= the_subsets_of_card 2,X by Lm1;
then reconsider h = h as Element of X' by A13;
set E = EqClass h,P';
reconsider E = EqClass h,P' as Element of P by EQREL_1:def 8;
F | (the_subsets_of_card 2,S) is Function of the_subsets_of_card 2,S, Seg 2 by A15, FUNCT_2:38;
then A16: F | (the_subsets_of_card 2,S) is constant by A11, A12, A14, FUNCT_2:188;
for x being set st x in the_subsets_of_card 2,S holds
x in E

let x be set ; :: thesis:
assume A17: x in the_subsets_of_card 2,S ; :: thesis:
then reconsider x' = x as Element of the_subsets_of_card 2,X by A15;
reconsider x'' = x as Element of X' by A15, A17;
A18: 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 A19: h in dom (F | (the_subsets_of_card 2,S)) by RELAT_1:90;
x' in (dom F) /\ (the_subsets_of_card 2,S) by A17, A18, XBOOLE_0:def 4;
then A20: x' in dom (F | (the_subsets_of_card 2,S)) by RELAT_1:90;
F . x' = (F | (the_subsets_of_card 2,S)) . x' by A17, FUNCT_1:72
.= (F | (the_subsets_of_card 2,S)) . h by A16, A20, A19, FUNCT_1:def 16
.= F . h by A12, FUNCT_1:72 ;
then A21: F1 . ((proj P') . x') = (F1 * (proj P')) . h by A18, FUNCT_1:22
.= F1 . ((proj P') . h) by A18, FUNCT_1:22 ;
(proj P') . x'' in P' ;
then ( h in E & (proj P') . h = (proj P') . x' ) by A8, A9, A21, EQREL_1:def 8, FUNCT_1:def 8;
hence x in E by Th13; :: thesis:

end;

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

end;

end;