let
R
be non
empty
Reflexive
MetrStruct
;
:: thesis:
for
S
being
Subset
of
R
st
S
is
bounded
holds
0
<=
diameter
S
let
S
be
Subset
of
R
;
:: thesis:
(
S
is
bounded
implies
0
<=
diameter
S
)
assume
A1
:
S
is
bounded
;
:: thesis:
0
<=
diameter
S
per
cases
(
S
=
{}
or
S
<>
{}
)
;
suppose
S
=
{}
;
:: thesis:
0
<=
diameter
S
hence
0
<=
diameter
S
by
Def8
;
:: thesis:
verum
end;
suppose
A2
:
S
<>
{}
;
:: thesis:
0
<=
diameter
S
set
x
= the
Element
of
S
;
reconsider
x
= the
Element
of
S
as
Element
of
R
by
A2
,
TARSKI:def 3
;
dist
(
x
,
x
)
<=
diameter
S
by
A1
,
A2
,
Def8
;
hence
0
<=
diameter
S
by
METRIC_1:1
;
:: thesis:
verum
end;
end;