let
X
,
Y
be
ext-real-membered
set
;
:: thesis:
max
(
(
inf
X
)
,
(
inf
Y
)
)
<=
inf
(
X
/\
Y
)
A1
:
inf
Y
is
LowerBound
of
Y
by
Def4
;
inf
X
is
LowerBound
of
X
by
Def4
;
then
max
(
(
inf
X
)
,
(
inf
Y
)
) is
LowerBound
of
X
/\
Y
by
A1
,
Th66
;
hence
max
(
(
inf
X
)
,
(
inf
Y
)
)
<=
inf
(
X
/\
Y
)
by
Def4
;
:: thesis:
verum