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