for R being non empty right_unital doubleLoopStr
for I being non empty left-ideal right-ideal Subset of R holds
( I is proper iff for u being Element of R st u is unital holds
not u in I )