(
n,k:
. (n E k) 
Min{ x | xrn } = Min{ x | xrk }) & (n:. n E Min{ x | xrn })
Prop. x E yx,y:. Dec(x E y)
x,y:. (x r y) (x E y) 
h:(). (n,k:. (n E k) h(n) = h(k)) & (n:. n E (h(n)))
z.Min{ x | xrz }
| 1 | (n,k:. (n E k) Min{ x | xrn } = Min{ x | xrk }) & (n:. n E Min{ x | xrn }) |
About:
 |  |  |  |  |
 |  |  |  |  |