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