let X be RealLinearSpace; :: thesis: for A being circled Subset of X holds A is symmetric
let A be circled Subset of X; :: thesis: A is symmetric
|.(- 1).| = - (- 1) by ABSVALUE:def 1
.= 1 ;
hence A = - A by Th28; :: according to RLTOPSP1:def 5 :: thesis: verum