let a be Real; :: thesis: for b being non zero Nat holds (frac (a / b)) * b < b
let b be non zero Nat; :: thesis: (frac (a / b)) * b < b
frac (a / b) < 1 by COMPLEX3:1;
then (frac (a / b)) * b < 1 * b by XREAL_1:68;
hence (frac (a / b)) * b < b ; :: thesis: verum