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