for i, j, m, n being Nat holds
( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n )