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 by Def14;
then A1: - (a - b) in I by IDEAL_1:14;
(b - a) - (- (a - b)) = (b - a) + (- (- (a - b))) by RLVECT_1:def 12
.= (b - a) + (a - b) by RLVECT_1:30
.= (b + (- a)) + (a - b) by RLVECT_1:def 12
.= b + ((- a) + (a - b)) by RLVECT_1:def 6
.= b + ((- a) + (a + (- b))) by RLVECT_1:def 12
.= b + (((- a) + a) + (- b)) by RLVECT_1:def 6
.= b + ((0. R) + (- b)) by RLVECT_1:16
.= b + (- b) by ALGSTR_1:def 5
.= 0. R by RLVECT_1:16 ;
then b - a = - (a - b) by RLVECT_1:35;
hence b,a are_congruent_mod I by A1, Def14; :: thesis: verum