let f be heterogeneous non empty real-valued FinSequence; :: thesis: Het f >= 2
set x = the Element of MeanLess f;
set y = the Element of MeanMore f;
HetSet f = (MeanLess f) \/ (MeanMore f) by MeanSum;
then A0: ( the Element of MeanLess f in HetSet f & the Element of MeanMore f in HetSet f ) by XBOOLE_0:def 3;
A4: the Element of MeanLess f <> the Element of MeanMore f by XBOOLE_0:3, MeanMiss;
A5: card { the Element of MeanLess f, the Element of MeanMore f} = 2 by CARD_2:57, A4;
card (Segm 2) c= card (Segm (Het f)) by A5, ZFMISC_1:32, A0, CARD_1:11;
hence Het f >= 2 by NAT_1:40; :: thesis: verum