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)

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

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 x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {a} or x in Class ((EqRel (R,{(0. R)})),a) )
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;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

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