let n be Nat; :: thesis: ex k being Nat st

( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 )

consider k being Nat such that

A1: not not n = (3 * k) + 0 & ... & not n = (3 * k) + (3 - 1) by Th22;

consider i being Nat such that

A2: ( 0 <= i & i <= 2 ) and

A3: n = (3 * k) + i by A1;

take k ; :: thesis: ( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 )

not not i = 0 & ... & not i = 2 by A2;

hence ( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 ) by A3; :: thesis: verum

( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 )

consider k being Nat such that

A1: not not n = (3 * k) + 0 & ... & not n = (3 * k) + (3 - 1) by Th22;

consider i being Nat such that

A2: ( 0 <= i & i <= 2 ) and

A3: n = (3 * k) + i by A1;

take k ; :: thesis: ( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 )

not not i = 0 & ... & not i = 2 by A2;

hence ( n = 3 * k or n = (3 * k) + 1 or n = (3 * k) + 2 ) by A3; :: thesis: verum