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 set st
( a in the carrier of R & x = Class (EqRel R,I),a ) by EQREL_1:def 5;
hence ex a being Element of R st x = Class (EqRel R,I),a ; :: thesis: verum