let i, j, m, n be Element of NAT ; :: thesis: ( max i,j,m,n = i or max i,j,m,n = j or max i,j,m,n = m or max i,j,m,n = n )
A1: ( max m,n = m or max m,n = n ) by XXREAL_0:16;
( max i,j = i or max i,j = j ) by XXREAL_0:16;
hence ( max i,j,m,n = i or max i,j,m,n = j or max i,j,m,n = m or max i,j,m,n = n ) by A1, XXREAL_0:16; :: thesis: verum