let
X
be
infinite
set
;
:: thesis:
for
A
being
Subset
of
X
st
A
is
finite
holds
A
`
is
infinite
let
A
be
Subset
of
X
;
:: thesis:
(
A
is
finite
implies
A
`
is
infinite
)
A
\/
(
A
`
)
=
[#]
X
by
SUBSET_1:10
.=
X
;
hence
(
A
is
finite
implies
A
`
is
infinite
) ;
:: thesis:
verum