for L being non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr
for I being non empty right-ideal Subset of L
for x being Element of L st x in I holds
- x in I