theorem Th9: :: POLYVIE1:9

for L being Field
for a, x being Element of L
for b being non zero Element of L holds
( x is_a_root_of <%a,b%> iff x = - (a / b) )