let R be Field; :: thesis: for S being Subset of R st S * S c= S & SQ R c= S holds
( S /\ (- S) = {(0. R)} iff not - (1. R) in S )
let S be Subset of R; :: thesis: ( S * S c= S & SQ R c= S implies ( S /\ (- S) = {(0. R)} iff not - (1. R) in S ) )
assume AS: ( S * S c= S & SQ R c= S ) ; :: thesis: ( S /\ (- S) = {(0. R)} iff not - (1. R) in S )
A0: 1. R in SQ R ;

X: now :: thesis: ( S /\ (- S) = {(0. R)} implies not - (1. R) in S )

assume A: S /\ (- S) = {(0. R)} ; :: thesis: not - (1. R) in S

now :: thesis: not - (1. R) in S

assume - (1. R) in S ; :: thesis: contradiction
then - (- (1. R)) in - S ;
then 1. R in S /\ (- S) by XBOOLE_0:def 4, A0, AS;
hence contradiction by A, TARSKI:def 1; :: thesis: verum

end;

hence not - (1. R) in S ; :: thesis: verum

end;

now :: thesis: ( not - (1. R) in S implies S /\ (- S) = {(0. R)} )

assume A: not - (1. R) in S ; :: thesis: S /\ (- S) = {(0. R)}

now :: thesis: not S /\ (- S) <> {(0. R)}

assume A2: S /\ (- S) <> {(0. R)} ; :: thesis: contradiction
B0: 0. R in SQ R ;
then - (0. R) in - S by AS;
then 0. R in S /\ (- S) by AS, B0, XBOOLE_0:def 4;
then A3: {(0. R)} c= S /\ (- S) by TARSKI:def 1;

now :: thesis: ex a being Element of R st
( a <> 0. R & a in S /\ (- S) )

assume A4: for a being Element of R holds
( not a <> 0. R or not a in S /\ (- S) ) ; :: thesis: contradiction

now :: thesis: for o being object st o in S /\ (- S) holds
o in {(0. R)}

let o be object ; :: thesis: ( o in S /\ (- S) implies o in {(0. R)} )
assume o in S /\ (- S) ; :: thesis: o in {(0. R)}
then o = 0. R by A4;
hence o in {(0. R)} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A2, A3, TARSKI:2; :: thesis: verum

end;

then consider a being Element of R such that
A5: ( a <> 0. R & a in S /\ (- S) ) ;
A9: ( a in S & a in - S ) by A5, XBOOLE_0:def 4;
then A6: - a in - (- S) ;

A7: now :: thesis: not - a = 0. R

assume - a = 0. R ; :: thesis: contradiction
then - (- a) = 0. R ;
hence contradiction by A5; :: thesis: verum

end;

((- a) ") ^2 is square ;
then ((- a) ") ^2 in SQ R ;
then A8: (((- a) ") ^2) * (- a) in S * S by AS, A6;
(- a) " in S

proof

(((- a) ") ^2) * (- a) = ((- a) ") * (((- a) ") * (- a)) by GROUP_1:def 3
.= ((- a) ") * (1. R) by A7, VECTSP_1:def 10
.= (- a) " ;
hence (- a) " in S by A8, AS; :: thesis: verum

end;

then A8: a * ((- a) ") in S * S by A9;
(- (a ")) * (- a) = a * (a ") by VECTSP_1:10
.= 1. R by A5, VECTSP_1:def 10 ;
then a * ((- a) ") = a * (- (a ")) by A7, VECTSP_1:def 10
.= - (a * (a ")) by VECTSP_1:8
.= - (1. R) by A5, VECTSP_1:def 10 ;
hence contradiction by A8, A, AS; :: thesis: verum

end;

hence S /\ (- S) = {(0. R)} ; :: thesis: verum

end;

hence ( S /\ (- S) = {(0. R)} iff not - (1. R) in S ) by X; :: thesis: verum