:: deftheorem defines <=' PRE_POLY:def 10 :
for n being Ordinal
for p, q being bag of n holds
( p <=' q iff ( p < q or p = q ) );