let L be non empty right_complementable add-associative right_zeroed right-distributive right_unital doubleLoopStr ; :: thesis: for S being Subset of L st 0. L in S & 1. L in S holds
for a being Element of L holds a in S + (a * S)
let S be Subset of L; :: thesis: ( 0. L in S & 1. L in S implies for a being Element of L holds a in S + (a * S) )
assume AS: ( 0. L in S & 1. L in S ) ; :: thesis: for a being Element of L holds a in S + (a * S)
let a be Element of L; :: thesis: a in S + (a * S)
a * (1. L) in { (a * i) where i is Element of L : i in S } by AS;
then (0. L) + (a * (1. L)) in { (c + b) where c, b is Element of L : ( c in S & b in a * S ) } by AS;
hence a in S + (a * S) ; :: thesis: verum