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