theorem Th52: :: POLYDIFF:52
Eval (0_. F_Real) = REAL --> 0