let X be RealLinearSpace; :: thesis: for A being symmetric Subset of X
for x being Point of X st x in A holds
- x in A
let A be symmetric Subset of X; :: thesis: for x being Point of X st x in A holds
- x in A
let x be Point of X; :: thesis: ( x in A implies - x in A )
assume A1: x in A ; :: thesis: - x in A
A = - A by Def5
.= (- 1) * A ;
then consider v being Point of X such that
A2: x = (- 1) * v and
A3: v in A by A1;
(- 1) * x = ((- 1) * (- 1)) * v by A2, RLVECT_1:def 7
.= v by RLVECT_1:def 8 ;
hence - x in A by A3, RLVECT_1:16; :: thesis: verum