thus Seg 8 = {1,2,3,4,5,6,7} \/ {(7 + 1)} by Th5, FINSEQ_1:9
.= {1,2,3,4,5,6,7,8} by ENUMSET1:28 ; :: thesis: verum