let
X
,
Y
be
ext-real-membered
set
;
:: thesis:
sup
(
X
/\
Y
)
<=
min
(
(
sup
X
)
,
(
sup
Y
)
)
A1
:
sup
Y
is
UpperBound
of
Y
by
Def3
;
sup
X
is
UpperBound
of
X
by
Def3
;
then
min
(
(
sup
X
)
,
(
sup
Y
)
) is
UpperBound
of
X
/\
Y
by
A1
,
Th65
;
hence
sup
(
X
/\
Y
)
<=
min
(
(
sup
X
)
,
(
sup
Y
)
)
by
Def3
;
:: thesis:
verum