let R be Ring; :: thesis: for I being Ideal of R

for a, b being Element of R holds

( Class ((EqRel (R,I)),a) = 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

( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )

let a, b be Element of R; :: thesis: ( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )

set E = EqRel (R,I);

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

then a in Class ((EqRel (R,I)),b) by Th5;

hence Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) by EQREL_1:23; :: thesis: verum

for a, b being Element of R holds

( Class ((EqRel (R,I)),a) = 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

( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )

let a, b be Element of R; :: thesis: ( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )

set E = EqRel (R,I);

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

proof

assume
a - b in I
; :: thesis: Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b)
assume
Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b)
; :: thesis: a - b in I

then a in Class ((EqRel (R,I)),b) by EQREL_1:23;

hence a - b in I by Th5; :: thesis: verum

end;then a in Class ((EqRel (R,I)),b) by EQREL_1:23;

hence a - b in I by Th5; :: thesis: verum

then a in Class ((EqRel (R,I)),b) by Th5;

hence Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) by EQREL_1:23; :: thesis: verum