let I be non degenerated commutative domRing-like Ring; :: thesis: I is_embedded_in the_Field_of_Quotients I
canHom I is RingMonomorphism by Th60;
hence I is_embedded_in the_Field_of_Quotients I by Def25; :: thesis: verum