( dom p = Segm n & dom q = Segm (m + n) ) by CARD_1:def 7;
hence (dom p) /\ (dom q) = dom p ; :: thesis: verum