let
i
be
Integer
;
:: thesis:
(
i
>=

1 &
i
<=
0
& not
i
=

1 implies
i
=
0
)
assume
that
A1
:
i
>=

1
and
A2
:
i
<=
0
;
:: thesis:
(
i
=

1 or
i
=
0
)
per
cases
(
i
<=

1 or
i
>

1 )
;
suppose
i
<=

1 ;
:: thesis:
(
i
=

1 or
i
=
0
)
hence
(
i
=

1 or
i
=
0
)
by
A1
,
XXREAL_0:1
;
:: thesis:
verum
end;
suppose
i
>

1 ;
:: thesis:
(
i
=

1 or
i
=
0
)
then
i
>=
(

1
)
+
1
by
INT_1:7
;
hence
(
i
=

1 or
i
=
0
)
by
A2
;
:: thesis:
verum
end;
end;