let X be RealLinearSpace; :: thesis: for B being non empty circled Subset of X holds 0. X in B
let B be non empty circled Subset of X; :: thesis: 0. X in B
|.0.| = 0 by ABSVALUE:2;
then 0 * B c= B by Def6;
then A1: {(0. X)} c= B by CONVEX1:34;
0. X in {(0. X)} by TARSKI:def 1;
hence 0. X in B by A1; :: thesis: verum