let i, j, m, n be Nat; :: thesis: ( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n )
A1: ( min (m,n) = m or min (m,n) = n ) by XXREAL_0:15;
( min (i,j) = i or min (i,j) = j ) by XXREAL_0:15;
hence ( min (i,j,m,n) = i or min (i,j,m,n) = j or min (i,j,m,n) = m or min (i,j,m,n) = n ) by A1, XXREAL_0:15; :: thesis: verum