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