theorem :: EXCHSORT:13

for f being Function holds f is sup (dom f) -limited ;