for I being non degenerated commutative domRing-like Ring holds I is_embedded_in the_Field_of_Quotients I