theorem Th2: :: STIRL2_1:2

for K, N being non empty Subset of NAT holds min ((min K),(min N)) = min (K \/ N)