let
a
be
Element
of
[.
0
,1
.]
;
:: thesis:
1

a
in
[.
0
,1
.]
(
0
<=
a
&
a
<=
1 )
by
XXREAL_1:1
;
then
( 1

1
<=
1

a
& 1

a
<=
1

0
)
by
XREAL_1:13
;
hence
1

a
in
[.
0
,1
.]
by
XXREAL_1:1
;
:: thesis:
verum