let
a
be
Real
;
:: thesis:
( 1
<
a
implies
(
1
/
a
)

1
<
0
)
assume
1
<
a
;
:: thesis:
(
1
/
a
)

1
<
0
then
1
/
a
<
1
/
1
by
XREAL_1:76
;
then
(
1
/
a
)

1
<
1

1
by
XREAL_1:9
;
hence
(
1
/
a
)

1
<
0
;
:: thesis:
verum