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