let
i
,
j
,
n
be
Nat
;
:: thesis:
(
i
<
j
&
j
in
Segm
n
implies
i
in
Segm
n
)
assume
that
A1
:
i
<
j
and
A2
:
j
in
Segm
n
;
:: thesis:
i
in
Segm
n
j
<
n
by
A2
,
NAT_1:44
;
then
i
<
n
by
A1
,
XXREAL_0:2
;
hence
i
in
Segm
n
by
NAT_1:44
;
:: thesis:
verum