Nuprl - Proof: least characterized2 1 1 2 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: least characterized2 1 1 2 1 1 1 1

1. p :

2. i :

3. p(i)
4. (least i:

. p(i))

{i:

(i+1)| p(i) & (

p(j)) }
5. x :

(i+1)
6. p(x)
7.

p(j)
8. j :

9. j<x

p(j)

By:	BackThru: Hyp:7

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html