let
r
be
Real
;
:: thesis:
(
0
<=
r
&
r
<=
1 implies (
0
<=
1

r
& 1

r
<=
1 ) )
assume
(
0
<=
r
&
r
<=
1 ) ;
:: thesis:
(
0
<=
1

r
& 1

r
<=
1 )
then
( 1

1
<=
1

r
& 1

r
<=
1

0
)
by
XREAL_1:13
;
hence
(
0
<=
1

r
& 1

r
<=
1 ) ;
:: thesis:
verum