let R be Ring; :: thesis: for a being Element of R holds Class (EqRel R,{(0. R)}),a = {a}
let a be Element of R; :: thesis: Class (EqRel R,{(0. R)}),a = {a}
set E = EqRel R,{(0. R)};
thus Class (EqRel R,{(0. R)}),a c= {a} :: according to XBOOLE_0:def 10 :: thesis: {a} c= Class (EqRel R,{(0. R)}),a

proof

let A be set ; :: according to TARSKI:def 3 :: thesis: ( not A in Class (EqRel R,{(0. R)}),a or A in {a} )
assume A1: A in Class (EqRel R,{(0. R)}),a ; :: thesis: A in {a}
then reconsider A = A as Element of R ;
[A,a] in EqRel R,{(0. R)} by A1, EQREL_1:27;
then A - a in {(0. R)} by Def5;
then A - a = 0. R by TARSKI:def 1;
then A = a by RLVECT_1:35;
hence A in {a} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} or x in Class (EqRel R,{(0. R)}),a )
assume x in {a} ; :: thesis: x in Class (EqRel R,{(0. R)}),a
then A2: x = a by TARSKI:def 1;
A3: a - a = 0. R by RLVECT_1:28;
0. R in {(0. R)} by TARSKI:def 1;
then [x,a] in EqRel R,{(0. R)} by A2, A3, Def5;
hence x in Class (EqRel R,{(0. R)}),a by EQREL_1:27; :: thesis: verum