let a be non integer Real; :: thesis: (frac a) + (frac (- a)) = 1
( frac a = a - [\a/] & frac (- a) = (- a) - [\(- a)/] ) by INT_1:def 8;
then (frac a) + (frac (- a)) = (- [\(a / 1)/]) - [\(- a)/]
.= ([\((- a) / 1)/] + 1) - [\(- (a / 1))/] by INT_1:63 ;
hence (frac a) + (frac (- a)) = 1 ; :: thesis: verum