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