let a be non integer Real; :: thesis: ( frac a = frac (- a) iff 2 * a is odd Integer )
( 2 * a is odd Integer implies frac a = frac (- a) )

proof

assume 2 * a is odd Integer ; :: thesis: frac a = frac (- a)
then reconsider n = ((2 * a) - 1) / 2 as Integer ;
( a = n + (1 / 2) & - a = (- (n + 1)) + (1 / 2) & 1 / (1 + 1) is light ) ;
hence frac a = frac (- a) ; :: thesis: verum

end;

hence ( frac a = frac (- a) iff 2 * a is odd Integer ) by EFR; :: thesis: verum