theorem :: EXCHSORT:14

for a, b being Ordinal
for f being Function st f is b -limited & a in dom f holds
a in b by ORDINAL2:19;