let R be Ring; :: thesis: for a being Element of R holds Class ((EqRel (R,([#] R))),a) = the carrier of R
let a be Element of R; :: thesis: Class ((EqRel (R,([#] R))),a) = the carrier of R
set E = EqRel (R,([#] R));
thus Class ((EqRel (R,([#] R))),a) c= the carrier of R ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of R c= Class ((EqRel (R,([#] R))),a)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in Class ((EqRel (R,([#] R))),a) )
assume x in the carrier of R ; :: thesis: x in Class ((EqRel (R,([#] R))),a)
then reconsider x = x as Element of R ;
x - a in [#] R ;
then [x,a] in EqRel (R,([#] R)) by Def5;
hence x in Class ((EqRel (R,([#] R))),a) by EQREL_1:19; :: thesis: verum