let R be non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr ; :: thesis: for I being Ideal of R
for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )
let I be Ideal of R; :: thesis: for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )
let a, b be Element of R; :: thesis: ( a in Class ((EqRel (R,I)),b) iff a - b in I )
set E = EqRel (R,I);

hereby :: thesis: ( a - b in I implies a in Class ((EqRel (R,I)),b) )

assume a in Class ((EqRel (R,I)),b) ; :: thesis: a - b in I
then [a,b] in EqRel (R,I) by EQREL_1:19;
hence a - b in I by Def5; :: thesis: verum

end;

assume a - b in I ; :: thesis: a in Class ((EqRel (R,I)),b)
then [a,b] in EqRel (R,I) by Def5;
hence a in Class ((EqRel (R,I)),b) by EQREL_1:19; :: thesis: verum