let X be RealLinearSpace; :: thesis: {(0. X)} is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( abs r <= 1 implies r * {(0. X)} c= {(0. X)} )
assume abs r <= 1 ; :: thesis: r * {(0. X)} c= {(0. X)}
thus r * {(0. X)} c= {(0. X)} by Th13; :: thesis: verum