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