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