theorem :: REALALG1:14

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for S being Subset of L
for a being Element of L holds
( a in S iff - a in - S )