let k, l be odd square Integer; :: thesis: (k - l) mod 8 = 0
reconsider k = k, l = l as odd Element of NAT by INT_1:3;
8 divides k - l by NEWTON03:19;
hence (k - l) mod 8 = 0 by INT_1:62; :: thesis: verum