let
p
be
Rational
;
:: thesis:
0
<
denominator
p
0
<>
denominator
p
by
Def3
;
hence
0
<
denominator
p
;
:: thesis:
verum