let R be Ring; :: thesis: for I being Ideal of R
for a being Element of holds Class (EqRel R,I),a is Element of
let I be Ideal of R; :: thesis: for a being Element of holds Class (EqRel R,I),a is Element of
let a be Element of ; :: thesis: Class (EqRel R,I),a is Element of
the carrier of (R / I) = Class (EqRel R,I) by Def6;
hence Class (EqRel R,I),a is Element of by EQREL_1:def 5; :: thesis: verum