theorem NF820: :: BINPACK1:33

for a being non empty positive at_most_one FinSequence of REAL
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,(NextFit a)) holds
for i, l, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k & 2 <= k & 1 <= l & l < k holds
(SumBin (a,(h . i),{l})) + (SumBin (a,(h . i),{(l + 1)})) > 1