let
n
be
Element
of
NAT
;
:: thesis:
( 1
<=
n
&
n
<=
2 & not
n
=
1 implies
n
=
2 )
assume
that
A1
: 1
<=
n
and
A2
:
n
<=
2 ;
:: thesis:
(
n
=
1 or
n
=
2 )
per
cases
(
n
=
1 or
n
>
1 )
by
A1
,
XXREAL_0:1
;
suppose
n
=
1 ;
:: thesis:
(
n
=
1 or
n
=
2 )
hence
(
n
=
1 or
n
=
2 ) ;
:: thesis:
verum
end;
suppose
n
>
1 ;
:: thesis:
(
n
=
1 or
n
=
2 )
then
n
>=
1
+
1
by
NAT_1:13
;
hence
(
n
=
1 or
n
=
2 )
by
A2
,
XXREAL_0:1
;
:: thesis:
verum
end;
end;