dom c is left_end by Def6;
hence not dom c is empty ; :: thesis: verum