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