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