theorem Th52: :: POLYDIFF:52

Eval (0_. F_Real) = REAL --> 0