let n be Nat; ex k being Nat st
( n = 8 * k or n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 )
consider k being Nat such that
A1:
not not n = (8 * k) + 0 & ... & not n = (8 * k) + (8 - 1)
by Th22;
consider i being Nat such that
A2:
( 0 <= i & i <= 7 )
and
A3:
n = (8 * k) + i
by A1;
take
k
; ( n = 8 * k or n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 )
not not i = 0 & ... & not i = 7
by A2;
hence
( n = 8 * k or n = (8 * k) + 1 or n = (8 * k) + 2 or n = (8 * k) + 3 or n = (8 * k) + 4 or n = (8 * k) + 5 or n = (8 * k) + 6 or n = (8 * k) + 7 )
by A3; verum