let a be non integer Real; :: thesis: ( - 1 < (frac a) - (frac (- a)) & (frac a) - (frac (- a)) < 1 )
( 2 * 0 < 2 * (frac a) & 2 * (frac a) < 2 * 1 ) by XREAL_1:68, INT_1:43;
then ( 0 - 1 < (2 * (frac a)) - 1 & (2 * (frac a)) - 1 < 2 - 1 ) by XREAL_1:9;
then ( - 1 < (2 * (frac a)) - ((frac a) + (frac (- a))) & (2 * (frac a)) - ((frac a) + (frac (- a))) < 1 ) by FRA;
hence ( - 1 < (frac a) - (frac (- a)) & (frac a) - (frac (- a)) < 1 ) ; :: thesis: verum