k:
, p:{p:(k
)| 
i:k. p(i) }. (least i:. p(i)) 
kk:, p:{p:(k)| i:k. p(i) }.
Thm* (least i:
. p(i)) {i:k| p(i) & (j:i. 
p(j)) }| Theorem | Name |
| k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i)) k | [least_wf] |
| cites the following: | |
| k:, p:{p:(k)| i:k. p(i) }.
Thm* (least i: . p(i)) {i:k| p(i) & (j:i. p(j)) } | [least_characterized] |