:: deftheorem Def4 defines max LEXBFS:def 5 :
for n being Ordinal
for T being connected TermOrder of n
for B being non empty finite Subset of (Bags n)
for b₄ being bag of n holds
( b₄ = max (B,T) iff ( b₄ in B & ( for x being bag of n st x in B holds
x <= b₄,T ) ) );