for R being Ring
for I being Ideal of R
for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)