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