let x be set ; ( not x in Seg 32 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 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 )
assume AS:
x in Seg 32
; ( 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 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 )
then reconsider j = x as Nat ;
( 1 <= j & j <= 32 )
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 or j = 1 + 16 or j = 1 + 17 or j = 1 + 18 or j = 1 + 19 or j = 1 + 20 or j = 1 + 21 or j = 1 + 22 or j = 1 + 23 or j = 1 + 24 or j = 1 + 25 or j = 1 + 26 or j = 1 + 27 or j = 1 + 28 or j = 1 + 29 or j = 1 + 30 or j = 1 + 31 )
by Lmseg32;
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 or x = 17 or x = 18 or x = 19 or x = 20 or x = 21 or x = 22 or x = 23 or x = 24 or x = 25 or x = 26 or x = 27 or x = 28 or x = 29 or x = 30 or x = 31 or x = 32 )
; verum