thus Seg 10 = (Seg 9) \/ {(9 + 1)} by FINSEQ_1:9
.= {1,2,3,4,5,6,7,8,9,10} by Th22, ENUMSET1:85 ; :: thesis: verum