p ^' q = p ^ ((2,(len q)) -cut q) by FINSEQ_6:def 5;
hence p ^' q is chordal ; :: thesis: verum