A1: rng c c= [#] T by Th24;
dom c is right_end by Def7;
then sup (dom c) in dom c by XXREAL_2:def 6;
then c . (sup (dom c)) in rng c by FUNCT_1:3;
hence c . (sup (dom c)) is Point of T by A1; :: thesis: verum