:: deftheorem Def4 defines max NAT_3:def 4 :
for X being set
for b1, b2 being real-valued ManySortedSet of X
for b₄ being ManySortedSet of X holds
( b₄ = max (b1,b2) iff for i being object holds
( ( b1 . i <= b2 . i implies b₄ . i = b2 . i ) & ( b1 . i > b2 . i implies b₄ . i = b1 . i ) ) );