for p being INT -valued Polynomial of F_Real
for e being Element of F_Real st e is_a_root_of p holds
for k, l being Integer st l <> 0 & e = k / l & k,l are_coprime holds
( k divides p . 0 & l divides LC p )