thus p ^ q is Element of D * by FINSEQ_1:def 11; :: thesis: verum