let a be Rational; :: thesis: (numerator (frac a)) mod (denominator (frac a)) = numerator (frac a)
numerator (frac a) in NAT by INT_1:3;
then reconsider x = numerator (frac a) as Nat ;
frac a < 1 by COMPLEX3:1;
hence (numerator (frac a)) mod (denominator (frac a)) = numerator (frac a) by NAT_D:24, RAT_1:35; :: thesis: verum