theorem NF815: :: BINPACK1:32

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, k being Nat st 1 <= i & i < len a & rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) holds
(SumBin (a,(h . (i + 1)),{k})) + (SumBin (a,(h . (i + 1)),{(k + 1)})) > 1