LogicSupplement Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  EquivRel x,y:T. E(x;y)
Def  == Refl(T;x,y.E(x;y)) & (Sym x,y:T. E(x;y)) & (Trans x,y:T. E(x;y))

is mentioned by

Thm*  R:(AAProp). 
Thm*  (EquivRel x,y:A. R(x,y))
Thm*  
Thm*  (x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z))))		[equivrel_characterization]
Def  EquivRel on A, R == EquivRel u,v:A. R(u,v)[equiv_rel_sep]

In prior sections: rel 1 quot 1

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

LogicSupplement Sections DiscrMathExt Doc