let
a
,
b
be
Element
of
[.
0
,1
.]
;
:: thesis:
a
*
b
in
[.
0
,1
.]
A0
: ( 1
>=
a
&
a
>=
0
& 1
>=
b
&
b
>=
0
)
by
XXREAL_1:1
;
then
1
>=
a
*
b
by
XREAL_1:160
;
hence
a
*
b
in
[.
0
,1
.]
by
XXREAL_1:1
,
A0
;
:: thesis:
verum