for L being non degenerated comRing
for p being non-zero Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff multiplicity (p,x) >= 1 )