take
aleph
(
succ
0
)
;
:: thesis:
( not
aleph
(
succ
0
)
is
limit_cardinal
&
aleph
(
succ
0
)
is
infinite
)
aleph
(
succ
0
)
=
nextcard
omega
by
CARD_1:19
,
CARD_1:46
;
hence
( not
aleph
(
succ
0
)
is
limit_cardinal
&
aleph
(
succ
0
)
is
infinite
) ;
:: thesis:
verum