theorem Th18: :: NAT_3:18

for X being set
for b1, b2 being real-valued finite-support ManySortedSet of X holds support (max (b1,b2)) c= (support b1) \/ (support b2)