let R be Ring; :: thesis: Class (EqRel (R,([#] R))) = { the carrier of R}
set E = EqRel (R,([#] R));
thus Class (EqRel (R,([#] R))) c= { the carrier of R} :: according to XBOOLE_0:def 10 :: thesis: { the carrier of R} c= Class (EqRel (R,([#] R)))

proof

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in Class (EqRel (R,([#] R))) or A in { the carrier of R} )
assume A in Class (EqRel (R,([#] R))) ; :: thesis: A in { the carrier of R}
then consider x being object such that
A1: x in the carrier of R and
A2: A = Class ((EqRel (R,([#] R))),x) by EQREL_1:def 3;
reconsider x = x as Element of R by A1;
Class ((EqRel (R,([#] R))),x) = the carrier of R

proof

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

end;

hence A in { the carrier of R} by A2, TARSKI:def 1; :: thesis: verum

end;

let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in { the carrier of R} or A in Class (EqRel (R,([#] R))) )
assume A in { the carrier of R} ; :: thesis: A in Class (EqRel (R,([#] R)))
then A = the carrier of R by TARSKI:def 1
.= Class ((EqRel (R,([#] R))),(0. R)) by Th7 ;
hence A in Class (EqRel (R,([#] R))) by EQREL_1:def 3; :: thesis: verum