theorem NF950: :: BINPACK1:36

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)) & rng f = Seg k holds
for j being Nat st 1 <= j & j <= k div 2 holds
(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1