dom c is right_end by Def7;
hence sup (dom c) is real ; :: thesis: verum