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