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 set ; :: 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:27; :: thesis: verum