theorem :: POLYDIFF:12

(id REAL) `| = REAL --> 1