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

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