theorem :: BINPACK1:44

for n being Nat st n is odd holds
ex a being non empty positive at_most_one FinSequence of REAL st
( len a = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
( n = card (rng f) & n = (2 * (Opt a)) - 1 ) ) )