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