0 <= n by NAT_1:2;
then A1: 0 + 1 <= n + 1 by XREAL_1:9;
take 1 ; :: thesis: ( 1 <= 1 & 1 <= n + 1 )
thus ( 1 <= 1 & 1 <= n + 1 ) by A1; :: thesis: verum