theorem X1: :: REALALG1:21

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