theorem :: NAT_6:27

for a being Integer holds Leg (a,2) = a mod 2