b,a:. ((a onto b))  ((b inj a))

By:	SimilarTo Thm*  f:(a onto b). (y.least x:. f(x)=y)  b inj a

1

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)

2 steps

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