let a, b, m be odd Nat; :: thesis: ( 4 divides a - b iff not 4 divides (a |^ m) + (b |^ m) )
thus ( 4 divides a - b implies not 4 divides (a |^ m) + (b |^ m) ) :: thesis: ( not 4 divides (a |^ m) + (b |^ m) implies 4 divides a - b )

proof

assume 4 divides a - b ; :: thesis: not 4 divides (a |^ m) + (b |^ m)
then not 4 divides a + b by Th58;
hence not 4 divides (a |^ m) + (b |^ m) by Th68; :: thesis: verum

end;

assume not 4 divides (a |^ m) + (b |^ m) ; :: thesis: 4 divides a - b
then not 4 divides a + b by Th68;
hence 4 divides a - b by Th58; :: thesis: verum