let R be non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr ; :: 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₁[ 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₁[x,y] holds
S₁[y,x]

proof

let x, y be object ; :: thesis: ( S₁[x,y] implies S₁[y,x] )
given P, Q being Element of R such that A2: ( P = x & Q = y & P - Q in I ) ; :: thesis: S₁[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;

A3: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[y,z] implies S₁[x,z] )
assume S₁[x,y] ; :: thesis: ( not S₁[y,z] or S₁[x,z] )
then consider P, Q being Element of R such that
A4: ( P = x & Q = y & P - Q in I ) ;
assume S₁[y,z] ; :: thesis: S₁[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;

A6: for x being object st x in the carrier of R holds
S₁[x,x]

proof

let x be object ; :: thesis: ( x in the carrier of R implies S₁[x,x] )
assume x in the carrier of R ; :: thesis: S₁[x,x]
then reconsider x = x as Element of R ;
x - x = 0. R by RLVECT_1:15;
hence S₁[x,x] by IDEAL_1:2; :: thesis: verum

end;

thus ex EqR being Equivalence_Relation of the carrier of R st
for x, y being object holds
( [x,y] in EqR iff ( x in the carrier of R & y in the carrier of R & S₁[x,y] ) ) from EQREL_1:sch 1(A6, A1, A3); :: thesis: verum