theorem Th19: :: RINGFRAC:12

for R being commutative Ring
for S being non empty multiplicatively-closed Subset of R
for x, y, z being Element of Frac S holds Fracadd (x,(Fracadd (y,z))) = Fracadd ((Fracadd (x,y)),z)