The generic symbol ORD1P2 only appears inside a THEORY. The many theorems referencing it are not listed here.