let R be non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of R
for a, b being Element of R st a,b are_congruent_mod I holds
b,a are_congruent_mod I
let I be non empty right-ideal Subset of R; :: thesis: for a, b being Element of R st a,b are_congruent_mod I holds
b,a are_congruent_mod I
let a, b be Element of R; :: thesis: ( a,b are_congruent_mod I implies b,a are_congruent_mod I )
assume a,b are_congruent_mod I ; :: thesis: b,a are_congruent_mod I
then a - b in I ;
then A1: - (a - b) in I by IDEAL_1:14;
(b - a) - (- (a - b)) = (b - a) + (- (- (a - b)))
.= (b - a) + (a - b) by RLVECT_1:17
.= (b + (- a)) + (a - b)
.= b + ((- a) + (a - b)) by RLVECT_1:def 3
.= b + ((- a) + (a + (- b)))
.= b + (((- a) + a) + (- b)) by RLVECT_1:def 3
.= b + ((0. R) + (- b)) by RLVECT_1:5
.= b + (- b) by ALGSTR_1:def 2
.= 0. R by RLVECT_1:5 ;
then b - a = - (a - b) by RLVECT_1:21;
hence b,a are_congruent_mod I by A1; :: thesis: verum