:: deftheorem Def4 defines min TERMORD:def 4 :
for n being Ordinal
for T being TermOrder of n
for b1, b2 being bag of n holds
( ( b1 <= b2,T implies min (b1,b2,T) = b1 ) & ( not b1 <= b2,T implies min (b1,b2,T) = b2 ) );