let
x
be
ExtReal
;
:: thesis:
0
<=
|.
x
.|
reconsider
x
=
x
as
R_eal
by
XXREAL_0:def 1
;
0
<=
|.
x
.|
;
hence
0
<=
|.
x
.|
;
:: thesis:
verum