let i, j, m, n be Element of 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