( dom p = dom (- p) & dom p is ordinal ) by VALUED_1:8;
hence - p is T-Sequence-like by ORDINAL1:def 7; :: thesis: verum