A1: rng c c= [#] T by Th24;
dom c is left_end by Def6;
then inf (dom c) in dom c by XXREAL_2:def 5;
then c . (inf (dom c)) in rng c by FUNCT_1:3;
hence c . (inf (dom c)) is Point of T by A1; :: thesis: verum