let x be set ; ( not x in 64 or x = 0 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 or x = 57 or x = 58 or x = 59 or x = 60 or x = 61 or x = 62 or x = 63 )
assume
x in 64
; ( x = 0 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 or x = 57 or x = 58 or x = 59 or x = 60 or x = 61 or x = 62 or x = 63 )
then
( x = 0 or ( x in Seg 64 & not x = 64 ) )
by th3;
hence
( x = 0 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 or x = 57 or x = 58 or x = 59 or x = 60 or x = 61 or x = 62 or x = 63 )
by Lmseg64a; verum