Def (P  Q)(L) == P(L) & Q(L)

is mentioned by

Thm* P,Q:(TProp), R:(TTProp). Thm* R preserves P  R preserves Q  R preserves P  Q

[and_preserved_by]

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