let R be Ring; :: thesis: for I being Ideal of R

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

let I be Ideal of R; :: thesis: for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)

let a be Element of R; :: thesis: Class ((EqRel (R,I)),a) is Element of (R / I)

the carrier of (R / I) = Class (EqRel (R,I)) by Def6;

hence Class ((EqRel (R,I)),a) is Element of (R / I) by EQREL_1:def 3; :: thesis: verum

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

let I be Ideal of R; :: thesis: for a being Element of R holds Class ((EqRel (R,I)),a) is Element of (R / I)

let a be Element of R; :: thesis: Class ((EqRel (R,I)),a) is Element of (R / I)

the carrier of (R / I) = Class (EqRel (R,I)) by Def6;

hence Class ((EqRel (R,I)),a) is Element of (R / I) by EQREL_1:def 3; :: thesis: verum