theorem Th17: :: NAT_3:17

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