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