let
j
,
l
be
Nat
;
:: thesis:
(
l
<=
j
or
l
=
j
+
1 or
j
+
2
<=
l
)
A1
:
(
j
+
1)
+
1
=
j
+
2 ;
(
l
<
j
+
1 or
l
=
j
+
1 or
j
+
1
<
l
)
by
XXREAL_0:1
;
hence
(
l
<=
j
or
l
=
j
+
1 or
j
+
2
<=
l
)
by
A1
,
NAT_1:13
;
:: thesis:
verum