let i, j, m, n be Element of NAT ; :: thesis: ( max i,j,m,n >= i & max i,j,m,n >= j & max i,j,m,n >= m & max i,j,m,n >= n )
A1: ( max m,n >= m & max m,n >= n ) by XXREAL_0:25;
A2: ( max i,j,m,n >= max i,j & max i,j,m,n >= max m,n ) by XXREAL_0:25;
( max i,j >= i & max i,j >= j ) by XXREAL_0:25;
hence ( max i,j,m,n >= i & max i,j,m,n >= j & max i,j,m,n >= m & max i,j,m,n >= n ) by A1, A2, XXREAL_0:2; :: thesis: verum