let a be non zero light Rational; :: thesis: not denominator a divides numerator a
|.((numerator a) / (denominator a)).| < 1 by COMPLEX3:1;
then |.(numerator a).| / |.(denominator a).| < 1 by COMPLEX1:67;
then |.(numerator a).| < |.(denominator a).| by XREAL_1:181;
hence not denominator a divides numerator a by INT_2:16, NAT_D:7; :: thesis: verum