take
omega
;
:: thesis:
(
omega
is
Element
of
M
&
omega
is
cardinal
&
omega
is
infinite
)
not
M
c=
omega
;
hence
omega
is
Element
of
M
by
ORDINAL1:16
;
:: thesis:
(
omega
is
cardinal
&
omega
is
infinite
)
thus
(
omega
is
cardinal
&
omega
is
infinite
) ;
:: thesis:
verum