let
x
be
Real
;
:: thesis:
(

.
x
.
<=
x
&
x
<=
.
x
.
)
per
cases
(
x
<
0
or
0
<=
x
)
;
suppose
A1
:
x
<
0
;
:: thesis:
(

.
x
.
<=
x
&
x
<=
.
x
.
)
then
.
x
.
=

x
by
Def1
;
hence
(

.
x
.
<=
x
&
x
<=
.
x
.
)
by
A1
;
:: thesis:
verum
end;
suppose
A2
:
0
<=
x
;
:: thesis:
(

.
x
.
<=
x
&
x
<=
.
x
.
)
then

x
<=

0
;
hence
(

.
x
.
<=
x
&
x
<=
.
x
.
)
by
A2
,
Def1
;
:: thesis:
verum
end;
end;