let a be non integer Real; :: thesis: ( frac a = frac (- a) implies 2 * a is odd Integer )
assume frac a = frac (- a) ; :: thesis: 2 * a is odd Integer
then (2 * [\a/]) + 1 = (2 * [\a/]) + ((frac a) + (frac a)) by FRA
.= 2 * ([\a/] + (frac a))
.= 2 * ([\a/] + (a - [\a/])) by INT_1:def 8
.= 2 * a ;
hence 2 * a is odd Integer ; :: thesis: verum