for L being non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed doubleLoopStr
for F being non empty Subset of L
for x being set holds
( x in F -LeftIdeal iff ex f being LeftLinearCombination of F st x = Sum f )