let i, j, m, n be Nat; :: thesis: ( i = min (i,j,m,n) implies ( i <= j & i <= m & i <= n ) )
A1: min (m,n) <= n by XXREAL_0:17;
assume i = min (i,j,m,n) ; :: thesis: ( i <= j & i <= m & i <= n )
then A2: ( i <= min (i,j) & i <= min (m,n) ) by XXREAL_0:17;
( min (i,j) <= j & min (m,n) <= m ) by XXREAL_0:17;
hence ( i <= j & i <= m & i <= n ) by A2, A1, XXREAL_0:2; :: thesis: verum