Def  Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c)

is mentioned

In prior sections: rel 1 DiscreteMath

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html