theorem :: BINPACK1:39

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 <= (2 * (Opt a)) - 1