let R be non empty right_complementable right-distributive add-associative right_zeroed left_zeroed doubleLoopStr ; :: thesis: for I being non empty right-ideal Subset of
for a being Element of holds a,a are_congruent_mod I
let I be non empty right-ideal Subset of ; :: thesis: for a being Element of holds a,a are_congruent_mod I
let a be Element of ; :: thesis: a,a are_congruent_mod I
( a - a = 0. R & 0. R in I ) by IDEAL_1:3, RLVECT_1:28;
hence a,a are_congruent_mod I by Def14; :: thesis: verum