let x be set ; ( not x in Seg 56 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 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 or x = 49 or x = 50 or x = 51 or x = 52 or x = 53 or x = 54 or x = 55 or x = 56 )
assume AS:
x in Seg 56
; ( 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 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 or x = 49 or x = 50 or x = 51 or x = 52 or x = 53 or x = 54 or x = 55 or x = 56 )
then reconsider j = x as Nat ;
( 1 <= j & j <= 1 + 55 )
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 or j = 1 + 32 or j = 1 + 33 or j = 1 + 34 or j = 1 + 35 or j = 1 + 36 or j = 1 + 37 or j = 1 + 38 or j = 1 + 39 or j = 1 + 40 or j = 1 + 41 or j = 1 + 42 or j = 1 + 43 or j = 1 + 44 or j = 1 + 45 or j = 1 + 46 or j = 1 + 47 or j = 1 + 48 or j = 1 + 49 or j = 1 + 50 or j = 1 + 51 or j = 1 + 52 or j = 1 + 53 or j = 1 + 54 or j = 1 + 55 )
by Lmseg56;
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 or x = 33 or x = 34 or x = 35 or x = 36 or x = 37 or x = 38 or x = 39 or x = 40 or x = 41 or x = 42 or x = 43 or x = 44 or x = 45 or x = 46 or x = 47 or x = 48 or x = 49 or x = 50 or x = 51 or x = 52 or x = 53 or x = 54 or x = 55 or x = 56 )
; verum