theorem :: REALALG1:22

for F being Field
for S being Subset of F st S * S c= S & S \/ (- S) = the carrier of F holds
( S /\ (- S) = {(0. F)} iff not - (1. F) in S )