let R be Ring; :: thesis: 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)

let I be Ideal of R; :: thesis: for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)

let x be Element of (R / I); :: thesis: ex a being Element of R st x = Class ((EqRel (R,I)),a)

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

then x in Class (EqRel (R,I)) ;

then ex a being object st

( a in the carrier of R & x = Class ((EqRel (R,I)),a) ) by EQREL_1:def 3;

hence ex a being Element of R st x = Class ((EqRel (R,I)),a) ; :: thesis: verum

for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)

let I be Ideal of R; :: thesis: for x being Element of (R / I) ex a being Element of R st x = Class ((EqRel (R,I)),a)

let x be Element of (R / I); :: thesis: ex a being Element of R st x = Class ((EqRel (R,I)),a)

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

then x in Class (EqRel (R,I)) ;

then ex a being object st

( a in the carrier of R & x = Class ((EqRel (R,I)),a) ) by EQREL_1:def 3;

hence ex a being Element of R st x = Class ((EqRel (R,I)),a) ; :: thesis: verum