seq (a,b) c= Seg (a + b) by Th7;
hence seq (a,b) is included_in_Seg by FINSEQ_1:def 13; :: thesis: verum