A: now :: thesis: for x being object st x in - (- S) holds
x in S

let x be object ; :: thesis: ( x in - (- S) implies x in S )
assume x in - (- S) ; :: thesis: x in S
then consider a being Element of L such that
A: ( x = - a & a in - S ) ;
consider b being Element of L such that
B: ( - b = a & b in S ) by A;
thus x in S by A, B; :: thesis: verum

end;

now :: thesis: for x being object st x in S holds
x in - (- S)

let x be object ; :: thesis: ( x in S implies x in - (- S) )
assume AS: x in S ; :: thesis: x in - (- S)
then reconsider y = x as Element of L ;
consider a being Element of L such that
A: ( - y = - a & a in S ) by AS;
consider b being Element of L such that
C: ( - b = - a & b in S ) by A;
B: - a in { (- s) where s is Element of L : s in S } by A;
y = - (- b) by A, C;
hence x in - (- S) by C, B; :: thesis: verum

end;

hence - (- S) = S by A, TARSKI:2; :: thesis: verum