Def (R1  R2)(x,y) == (x R1 y)  (x R2 y)

is mentioned by

Thm* P:(TProp), R1,R2:(TTProp). Thm* R1 preserves P  R2 preserves P  R1  R2 preserves P	[preserved_by_or]
Thm* R1,R2:(TTProp). Thm* (Sym x,y:T. x R1 y)  (Sym x,y:T. x R2 y)  (Sym x,y:T. x (R1  R2) y)	[symmetric_rel_or]

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