let f be Function; :: thesis: f is limit- f -limited
limit- f = sup (dom f) by Th005;
hence f is limit- f -limited by LI; :: thesis: verum