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 object ; :: 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:19;
then A - a in {(0. R)} by Def5;
then A - a = 0. R by TARSKI:def 1;
then A = a by RLVECT_1:21;
hence A in {a} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: 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;
( a - a = 0. R & 0. R in {(0. R)} ) by RLVECT_1:15, TARSKI:def 1;
then [x,a] in EqRel (R,{(0. R)}) by A2, Def5;
hence x in Class ((EqRel (R,{(0. R)})),a) by EQREL_1:19; :: thesis: verum