theorem Th25: :: BCIALG_5:25

for i, j, m, n being Nat st i = min (i,j,m,n) holds
( i <= j & i <= m & i <= n )