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 )

proof

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:31;
hence a - b in I by Th5; :: thesis: verum

end;

assume a - b in I ; :: thesis: 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:31; :: thesis: verum