let n be Nat; :: thesis: ( 3 divides n or 3 divides n + 1 or 3 divides n + 2 )
( 3 divides n - 1 iff 3 divides n + 2 )

proof

hereby :: thesis: ( 3 divides n + 2 implies 3 divides n - 1 )

assume C1: 3 divides n - 1 ; :: thesis: 3 divides n + 2
3 divides (n - 1) + 3 by C1, WSIERP_1:4;
hence 3 divides n + 2 ; :: thesis: verum

end;

assume 3 divides n + 2 ; :: thesis: 3 divides n - 1
then 3 divides (n + 2) - 3 by PREPOWER:94;
hence 3 divides n - 1 ; :: thesis: verum

end;

hence ( 3 divides n or 3 divides n + 1 or 3 divides n + 2 ) by NEWTON02:188; :: thesis: verum