p:(
a
). {x:a| p(x) } ~ (size(a)(p))f:(a2).
Thm* (
i:a. P(i) 
f(i) = 1 
2) 
({x:a| P(x) } ~ (Msize(f)))| Rank | Theorem | Name |
| 9 | p:(a). {x:a| p(x) } ~ (size(a)(p)) | [card_st_vs_boolsize] |
| cites the following: | ||
| 8 | f:(a2).
Thm* ( i:a. P(i) f(i) = 1 2) ({x:a| P(x) } ~ (Msize(f))) | [card_st_vs_msize] |