p:{p:(
)| 
i:. p(i) }. (least i:. p(i)) 
p:{p:()| i:. p(i) }.
Thm* (least i:
. p(i)) {i:| p(i) & (j:. j<i 
p(j)) }| Rank | Theorem | Name |
| 2 | p:{p:()| i:. p(i) }. (least i:. p(i)) | [least_wf2] |
| cites the following: | ||
| 1 | p:{p:()| i:. p(i) }.
Thm* (least i: . p(i)) {i:| p(i) & (j:. j<i p(j)) } | [least_characterized2] |