thus Seg 5 = {1,2,3,4} \/ {(4 + 1)} by Th2, FINSEQ_1:11
.= {1,2,3,4,5} by ENUMSET1:50 ; :: thesis: verum