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

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