let
a
,
b
be
Real
;
:: thesis:
(
0
<
a
& 1
<
b
implies
(
a
/
b
)

a
<
0
)
assume
that
A1
:
0
<
a
and
A2
: 1
<
b
;
:: thesis:
(
a
/
b
)

a
<
0
A3
:
(
a
/
b
)

a
=
a
*
(
(
1
/
b
)

1
)
;
(
1
/
b
)

1
<
0
by
A2
,
Th07
;
hence
(
a
/
b
)

a
<
0
by
A1
,
A3
;
:: thesis:
verum