theorem Th11: :: RING_1:11

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