dom c is right_end by Def7;
hence not dom c is empty ; :: thesis: verum