let
A
be
ext-real-membered
set
;
:: thesis:
(
sup
A
=
inf
A
implies
A
=
{
(
inf
A
)
}
)
assume
A1
:
sup
A
=
inf
A
;
:: thesis:
A
=
{
(
inf
A
)
}
then
A
c=
[.
(
inf
A
)
,
(
inf
A
)
.]
by
Th69
;
then
A2
:
A
c=
{
(
inf
A
)
}
by
XXREAL_1:17
;
A
<>
{}
by
A1
,
Th38
,
Th39
;
hence
A
=
{
(
inf
A
)
}
by
A2
,
ZFMISC_1:33
;
:: thesis:
verum