dom p = dom (- p) by VALUED_1:8;
hence - p is finite by FINSET_1:29; :: thesis: verum