let f be real-valued FinSequence; :: thesis: HetSet f = (MeanLess f) \/ (MeanMore f)
thus HetSet f c= (MeanLess f) \/ (MeanMore f) :: according to XBOOLE_0:def 10 :: thesis: (MeanLess f) \/ (MeanMore f) c= HetSet f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in HetSet f or x in (MeanLess f) \/ (MeanMore f) )
assume x in HetSet f ; :: thesis: x in (MeanLess f) \/ (MeanMore f)
then consider i being Nat such that
A1: ( i = x & i in dom f & f . i <> Mean f ) ;
( f . i < Mean f or f . i > Mean f ) by A1, XXREAL_0:1;
then ( i in MeanLess f or i in MeanMore f ) by A1;
hence x in (MeanLess f) \/ (MeanMore f) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (MeanLess f) \/ (MeanMore f) or x in HetSet f )
assume x in (MeanLess f) \/ (MeanMore f) ; :: thesis: x in HetSet f

per cases then ( x in MeanLess f or x in MeanMore f ) by XBOOLE_0:def 3;

suppose x in MeanLess f ; :: thesis: x in HetSet f

then ex i being Nat st
( i = x & i in dom f & f . i < Mean f ) ;
hence x in HetSet f ; :: thesis: verum

end;

suppose x in MeanMore f ; :: thesis: x in HetSet f

then ex i being Nat st
( i = x & i in dom f & f . i > Mean f ) ;
hence x in HetSet f ; :: thesis: verum

end;

end;