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
( a - a = 0. R & 0. R in I ) by IDEAL_1:3, RLVECT_1:15;
hence a,a are_congruent_mod I ; :: thesis: verum