let
X
be
set
;
:: thesis:
( not
X
is
finite
implies
card
X
=
omega
*`
(
card
X
)
)
assume
A1
: not
X
is
finite
;
:: thesis:
card
X
=
omega
*`
(
card
X
)
then
omega
c=
card
X
by
CARD_3:85
;
hence
card
X
=
omega
*`
(
card
X
)
by
A1
,
Th16
;
:: thesis:
verum