for p being INT -valued monic Polynomial of F_Real
for e being rational Element of F_Real st e is_a_root_of p holds
e is integer