for I being non degenerated commutative domRing-like Ring
for u, v, w being Element of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w) by Th20;