Def P & Q == PQ

is mentioned by

Def Bij(A; B; f) == Inj(A; B; f) & Surj(A; B; f)	[biject]
Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id	[inv_funs]

In prior sections: core

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