Def  S  T == x:S. x  T

is mentioned by

Thm*  (A bij B)  (A onto B)	[bijection_type_inc_surj]
Thm*  (A bij B)  (A onto B)	[bijtype_sub_surjtype]
Thm*  (A bij B)  (A inj B)	[bijection_type_inc_inj]
Thm*  (A bij B)  (A inj B)	[bijtype_sub_injtype]

In prior sections: quot 1 LogicSupplement int 1

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