k:
, p:{p:(k
)| 
i:k. p(i) }, j:(least i:. p(i)). 
p(j)k:, 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) }, j:(least i:. p(i)). p(j) | [least_is_least] |
| 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] |