( rng (X --> o) c= {o} & {o} c= succ o ) by FUNCOP_1:13, XBOOLE_1:7;
then rng (X --> o) c= succ o ;
hence X --> o is Ordinal-yielding ; :: thesis: verum