let S be Subset of X; :: thesis: ( S is empty implies S is circled )
assume S is empty ; :: thesis: S is circled
then X: S = {} X ;
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( abs r <= 1 implies r * S c= S )
thus ( abs r <= 1 implies r * S c= S ) by CONVEX1:33, X; :: thesis: verum