let
A
be
Interval
;
:: thesis:
diameter
A
>=
0
per
cases
(
A
is
empty
or not
A
is
empty
)
;
suppose
A
is
empty
;
:: thesis:
diameter
A
>=
0
hence
diameter
A
>=
0
by
Def6
;
:: thesis:
verum
end;
suppose
not
A
is
empty
;
:: thesis:
diameter
A
>=
0
then
inf
A
<=
sup
A
by
XXREAL_2:40
;
then
(
sup
A
)

(
inf
A
)
>=
0
by
XXREAL_3:40
;
hence
diameter
A
>=
0
by
Def6
;
:: thesis:
verum
end;
end;