1. b : 
2. a : 
3. f:(a onto b). (y.least x:. f(x)=y)  b inj a
4. (a onto b)
  (b inj a)

1

4. f : (a onto b) 5. (y.least x:. f(x)=y)  b inj a   (b inj a)

1 step

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