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
abs (- 1) = - (- 1) by ABSVALUE:def 1
.= 1 ;
hence A = - A by Th29; :: according to RLTOPSP1:def 5 :: thesis: verum