let
a
,
b
be
Element
of
[.
0
,1
.]
;
:: thesis:
max
(
a
,
b
)
in
[.
0
,1
.]
(
max
(
a
,
b
)
=
a
or
max
(
a
,
b
)
=
b
)
by
XXREAL_0:16
;
hence
max
(
a
,
b
)
in
[.
0
,1
.]
;
:: thesis:
verum