let
p
be
Rational
;
:: thesis:
1
<=
denominator
p
0
+
1
<=
denominator
p
by
NAT_1:13
;
hence
1
<=
denominator
p
;
:: thesis:
verum