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 R
for a being Element of R holds a,a are_congruent_mod I
let I be non empty right-ideal Subset of R; :: thesis: for a being Element of R holds a,a are_congruent_mod I
let a be Element of R; :: thesis: a,a are_congruent_mod I
A1: a - a = 0. R by RLVECT_1:28;
0. R in I by IDEAL_1:3;
hence a,a are_congruent_mod I by A1, Def14; :: thesis: verum