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