let R be Ring; :: thesis: for I being Ideal of R ex E being Equivalence_Relation of the carrier of R st

for x, y being object holds

( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st

( P = x & Q = y & P - Q in I ) ) )

let I be Ideal of R; :: thesis: ex E being Equivalence_Relation of the carrier of R st

for x, y being object holds

( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st

( P = x & Q = y & P - Q in I ) ) )

defpred S_{1}[ object , object ] means ex P, Q being Element of R st

( P = $1 & Q = $2 & P - Q in I );

A1: for x, y being object st S_{1}[x,y] holds

S_{1}[y,x]
_{1}[x,y] & S_{1}[y,z] holds

S_{1}[x,z]

S_{1}[x,x]

for x, y being object holds

( [x,y] in EqR iff ( x in the carrier of R & y in the carrier of R & S_{1}[x,y] ) )
from EQREL_1:sch 1(A6, A1, A3); :: thesis: verum

for x, y being object holds

( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st

( P = x & Q = y & P - Q in I ) ) )

let I be Ideal of R; :: thesis: ex E being Equivalence_Relation of the carrier of R st

for x, y being object holds

( [x,y] in E iff ( x in the carrier of R & y in the carrier of R & ex P, Q being Element of R st

( P = x & Q = y & P - Q in I ) ) )

defpred S

( P = $1 & Q = $2 & P - Q in I );

A1: for x, y being object st S

S

proof

A3:
for x, y, z being object st S
let x, y be object ; :: thesis: ( S_{1}[x,y] implies S_{1}[y,x] )

given P, Q being Element of R such that A2: ( P = x & Q = y & P - Q in I ) ; :: thesis: S_{1}[y,x]

take Q ; :: thesis: ex Q being Element of R st

( Q = y & Q = x & Q - Q in I )

take P ; :: thesis: ( Q = y & P = x & Q - P in I )

- (P - Q) = Q - P by RLVECT_1:33;

hence ( Q = y & P = x & Q - P in I ) by A2, IDEAL_1:13; :: thesis: verum

end;given P, Q being Element of R such that A2: ( P = x & Q = y & P - Q in I ) ; :: thesis: S

take Q ; :: thesis: ex Q being Element of R st

( Q = y & Q = x & Q - Q in I )

take P ; :: thesis: ( Q = y & P = x & Q - P in I )

- (P - Q) = Q - P by RLVECT_1:33;

hence ( Q = y & P = x & Q - P in I ) by A2, IDEAL_1:13; :: thesis: verum

S

proof

A6:
for x being object st x in the carrier of R holds
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[y,z] implies S_{1}[x,z] )

assume S_{1}[x,y]
; :: thesis: ( not S_{1}[y,z] or S_{1}[x,z] )

then consider P, Q being Element of R such that

A4: ( P = x & Q = y & P - Q in I ) ;

assume S_{1}[y,z]
; :: thesis: S_{1}[x,z]

then consider W, S being Element of R such that

A5: ( W = y & S = z & W - S in I ) ;

take P ; :: thesis: ex Q being Element of R st

( P = x & Q = z & P - Q in I )

take S ; :: thesis: ( P = x & S = z & P - S in I )

(P - Q) + (Q - S) = ((P - Q) + Q) - S by RLVECT_1:28

.= P - S by Th1 ;

hence ( P = x & S = z & P - S in I ) by A4, A5, IDEAL_1:def 1; :: thesis: verum

end;assume S

then consider P, Q being Element of R such that

A4: ( P = x & Q = y & P - Q in I ) ;

assume S

then consider W, S being Element of R such that

A5: ( W = y & S = z & W - S in I ) ;

take P ; :: thesis: ex Q being Element of R st

( P = x & Q = z & P - Q in I )

take S ; :: thesis: ( P = x & S = z & P - S in I )

(P - Q) + (Q - S) = ((P - Q) + Q) - S by RLVECT_1:28

.= P - S by Th1 ;

hence ( P = x & S = z & P - S in I ) by A4, A5, IDEAL_1:def 1; :: thesis: verum

S

proof

thus
ex EqR being Equivalence_Relation of the carrier of R st
let x be object ; :: thesis: ( x in the carrier of R implies S_{1}[x,x] )

assume x in the carrier of R ; :: thesis: S_{1}[x,x]

then reconsider x = x as Element of R ;

x - x = 0. R by RLVECT_1:15;

hence S_{1}[x,x]
by IDEAL_1:2; :: thesis: verum

end;assume x in the carrier of R ; :: thesis: S

then reconsider x = x as Element of R ;

x - x = 0. R by RLVECT_1:15;

hence S

for x, y being object holds

( [x,y] in EqR iff ( x in the carrier of R & y in the carrier of R & S