(
f
in
<^
a
,
b
^>
&
<^
a
,
b
^>
c=
MonFuncs
(
(
latt
a
)
,
(
latt
b
)
) )
by
A1
,
Def4
;
then
ex
g
being
Function
of
(
latt
a
)
,
(
latt
b
)
st
(
f
=
g
&
g
in
Funcs
( the
carrier
of
(
latt
a
)
, the
carrier
of
(
latt
b
)
) &
g
is
monotone
)
by
ORDERS_3:def 6
;
hence
f
is
monotone
Function
of
(
latt
a
)
,
(
latt
b
)
;
:: thesis:
verum