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

now :: thesis: ( - a in - S implies a in S )

assume - a in - S ; :: thesis: a in S
then - (- a) in - (- S) ;
hence a in S ; :: thesis: verum

end;

hence ( a in S iff - a in - S ) ; :: thesis: verum