let I be non degenerated commutative domRing-like Ring; :: thesis: the_Field_of_Quotients I is non empty commutative doubleLoopStr
for x, y being Element of (the_Field_of_Quotients I) holds x * y = y * x by Th24;
hence the_Field_of_Quotients I is non empty commutative doubleLoopStr by GROUP_1:def 12; :: thesis: verum