Def R preserves P == x,y:T. P(x)  (x R y)  P(y)

is mentioned by

Thm* P,Q:(TProp), R:(TTProp). Thm* R preserves P  R preserves Q  R preserves P  Q	[and_preserved_by]
Thm* P:(TProp), R1,R2:(TTProp). Thm* R1 preserves P  R2 preserves P  R1  R2 preserves P	[preserved_by_or]
Thm* P:(TProp), R:(TTProp). R preserves P  R^* preserves P	[preserved_by_star]
Thm* P:(TProp), R1,R2:(TTProp). Thm* (x,y:T. (x R1 y)  (x R2 y))  R2 preserves P  R1 preserves P	[preserved_by_monotone]

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