:: deftheorem defines min BCIALG_5:def 4 :
for i, j, m, n being Nat holds min (i,j,m,n) = min ((min (i,j)),(min (m,n)));