let
r
be
irrational
Real
;
:: thesis:
(
HWZSet
r
is
finite
implies
HWZSet1
r
is
finite
)
TRANQN
.:
(
HWZSet
r
)
=
HWZSet1
r
by
Th6
;
hence
(
HWZSet
r
is
finite
implies
HWZSet1
r
is
finite
) ;
:: thesis:
verum