theorem Th12: :: RING_1:12

for R being non empty right_complementable distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
for I being Ideal of R
for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)