:: deftheorem defines MeanLess RVSUM_3:def 7 :
for f being real-valued FinSequence holds MeanLess f = { n where n is Nat : ( n in dom f & f . n < Mean f ) } ;