::
deftheorem
defines
inf
SUPINF_2:def 2 :
for
D
being
ext-real-membered
set
for
X
being
set
for
Y
being
Subset
of
D
for
F
being
PartFunc
of
X
,
Y
holds
inf
F
=
inf
(
rng
F
)
;