is mentioned by

Thm*  InvFuns(A;B;f;g)  Inj(A; B; f) & Inj(B; A; g)	[invfuns_are_inj]
Thm*  InvFuns(A;B;f;g)  Surj(A; B; f) & Surj(B; A; g)	[invfuns_are_surj]

In prior sections: core well fnd int 1 bool 1 rel 1 LogicSupplement int 2 num thy 1 IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html