let R be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum