1. B : Type
2. e : BB
3. IsEqFun(B;e)
4. a : 
5. f : aB
6. Surj(a; B; f)
7. f  a onto B
  (y.least x:. (f(x)) e y)  B inj a

By:	(y,x. (f(x)) e y)  B{p:(a)| i:a. p(i) } | (y.least x:. (f(x)) e y)  Ba Asserted

1	(y,x. (f(x)) e y)  B{p:(a)| i:a. p(i) }	4 steps
2	8. (y,x. (f(x)) e y)  B{p:(a)| i:a. p(i) }   (y.least x:. (f(x)) e y)  Ba	1 step
3	8. (y,x. (f(x)) e y)  B{p:(a)| i:a. p(i) } 9. (y.least x:. (f(x)) e y)  Ba   (y.least x:. (f(x)) e y)  B inj a	6 steps

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