dom c is left_end by Def6;
hence inf (dom c) is real ; :: thesis: verum