let
p
be
Rational
;
:: thesis:
1
#Q
p
=
1
thus
1
#Q
p
=
(
denominator
p
)
-Root
1
by
Th37
.= 1
by
Th20
,
RAT_1:11
;
:: thesis:
verum