set
f
= the
monotone
Function
of
S
,
T
;
the
monotone
Function
of
S
,
T
in
Funcs
( the
carrier
of
S
, the
carrier
of
T
)
by
FUNCT_2:8
;
hence
not
MonMaps
(
S
,
T
) is
empty
by
YELLOW_1:def 6
;
:: thesis:
verum