let
x
be
ExtReal
;
:: thesis:
(

.
x
.
<=
x
&
x
<=
.
x
.
)
reconsider
x
=
x
as
R_eal
by
XXREAL_0:def 1
;
per
cases
(
0
<=
x
or not
0
<=
x
)
;
suppose
A1
:
0
<=
x
;
:: thesis:
(

.
x
.
<=
x
&
x
<=
.
x
.
)
thus
(

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

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

x
by
Def1
;
hence
(

.
x
.
<=
x
&
x
<=
.
x
.
) ;
:: thesis:
verum
end;
end;