take 1 ; :: thesis: ( 1 <= 1 & 1 <= n + 1 )
0 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:7;
hence ( 1 <= 1 & 1 <= n + 1 ) ; :: thesis: verum