:: deftheorem defOpt defines Opt BINPACK1:def 4 :
for a being non empty at_most_one FinSequence of REAL
for b₂ being Element of NAT holds
( b₂ = Opt a iff ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & b₂ = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
b₂ <= card (rng f) ) ) );