theorem :: CFUNCT_1:73

for X being set
for C being non empty set
for f being PartFunc of C,COMPLEX holds |.f.| | X is bounded_below