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