let a, b be odd square Element of NAT ; :: thesis: 8 divides a - b
consider c being Nat such that
A1: a = c ^2 by PYTHTRIP:def 3;
consider d being Nat such that
A2: b = d ^2 by PYTHTRIP:def 3;
( c is odd & d is odd & a = c |^ 2 & b = d |^ 2 ) by A1, A2;
hence 8 divides a - b by NEWTON02:63; :: thesis: verum