theorem :: BINPACK1:30

for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1