A7
:
dom
g
=
X
by
FUNCT_2:def 1
;
A8
:
dom
(
leq
(
f
,
g
)
)
=
(
dom
f
)
/\
(
dom
g
)
by
Def5
;
A9
:
dom
f
=
X
by
FUNCT_2:def 1
;
rng
(
leq
(
f
,
g
)
)
c=
INT
;
hence
leq
(
f
,
g
) is
Function
of
X
,
INT
by
A8
,
A9
,
A7
,
FUNCT_2:2
;
:: thesis:
verum