let R be non empty right_complementable add-associative right_zeroed addLoopStr ; for I being non empty add-closed Subset of R
for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds
a,c are_congruent_mod I
let I be non empty add-closed Subset of R; for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds
a,c are_congruent_mod I
let a, b, c be Element of R; ( a,b are_congruent_mod I & b,c are_congruent_mod I implies a,c are_congruent_mod I )
assume
( a,b are_congruent_mod I & b,c are_congruent_mod I )
; a,c are_congruent_mod I
then
( a - b in I & b - c in I )
;
then A1:
(a - b) + (b - c) in I
by IDEAL_1:def 1;
(a - b) + (b - c) =
(a + (- b)) + (b - c)
.=
a + ((- b) + (b - c))
by RLVECT_1:def 3
.=
a + ((- b) + (b + (- c)))
.=
a + (((- b) + b) + (- c))
by RLVECT_1:def 3
.=
a + ((0. R) + (- c))
by RLVECT_1:5
.=
a + (- c)
by ALGSTR_1:def 2
.=
a - c
;
hence
a,c are_congruent_mod I
by A1; verum