let x be set ; ( not x in Seg 16 or x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 )
assume AS:
x in Seg 16
; ( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 )
then reconsider j = x as Nat ;
( 1 <= j & j <= 16 )
by AS, FINSEQ_1:1;
then
( j = 1 or j = 1 + 1 or j = 1 + 2 or j = 1 + 3 or j = 1 + 4 or j = 1 + 5 or j = 1 + 6 or j = 1 + 7 or j = 1 + 8 or j = 1 + 9 or j = 1 + 10 or j = 1 + 11 or j = 1 + 12 or j = 1 + 13 or j = 1 + 14 or j = 1 + 15 )
by Lmseg16;
hence
( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 or x = 7 or x = 8 or x = 9 or x = 10 or x = 11 or x = 12 or x = 13 or x = 14 or x = 15 or x = 16 )
; verum