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