let b be Nat; :: thesis: ( 3 divides b or 3 divides b - 1 or 3 divides b + 1 )
( (2 * 1) + 1 = 3 & b |^ 1 = b ) ;
hence ( 3 divides b or 3 divides b - 1 or 3 divides b + 1 ) by Th70, PEPIN:41; :: thesis: verum