for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT
for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds
k div 2 < Sum a