Def AB == B<A

is mentioned by

Thm* i:, A:({i...}Prop). (j:. ij  A(j))  (j:{i...}. A(j))	[int_le_to_int_upper]
Thm* i,j:, y:{i...j}. iy & yj	[int_iseg_properties]
Thm* i:, j:{...i}. ji	[int_lower_properties]
Thm* i:, j:{i...}. ij	[int_upper_properties]
Def {i...j} == {k:| ik & kj }	[int_iseg]
Def {...i} == {j:| ji }	[int_lower]
Def {i...} == {j:| ij }	[int_upper]
Def  == {i:| 0i }	[nat]
Def i  j  k == ij & jk	[lele]
Def i  j < k == ij & j<k	[lelt]

In prior sections: core

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