theorem Th12: :: EXCHSORT:12

for f being Function holds f is inf (dom f) -based by ORDINAL2:14, ORDINAL2:17;