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)))

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

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 { the carrier of R} or A in Class (EqRel (R,([#] R))) )
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

end;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

hence
A in { the carrier of R}
by A2, TARSKI:def 1; :: thesis: verum
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;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

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