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