let
F
be non
empty
finite
set
;
:: thesis:
(
card
F
)

1
=
(
card
F
)
'
1
(
card
F
)

1
>=
0
by
NAT_1:14
,
XREAL_1:48
;
hence
(
card
F
)

1
=
(
card
F
)
'
1
by
XREAL_0:def 2
;
:: thesis:
verum