thus ( M is circled implies for u being VECTOR of V
for r being Real st |.r.| <= 1 & u in M holds
r * u in M ) :: thesis: ( ( for u being VECTOR of V
for r being Real st |.r.| <= 1 & u in M holds
r * u in M ) implies M is circled )

proof

assume A1: M is circled ; :: thesis: for u being VECTOR of V
for r being Real st |.r.| <= 1 & u in M holds
r * u in M
let u be VECTOR of V; :: thesis: for r being Real st |.r.| <= 1 & u in M holds
r * u in M
let r be Real; :: thesis: ( |.r.| <= 1 & u in M implies r * u in M )
assume |.r.| <= 1 ; :: thesis: ( not u in M or r * u in M )
then A2: r * M c= M by A1;
assume u in M ; :: thesis: r * u in M
then r * u in r * M by RLTOPSP1:1;
hence r * u in M by A2; :: thesis: verum

end;

assume A3: for u being VECTOR of V
for r being Real st |.r.| <= 1 & u in M holds
r * u in M ; :: thesis: M is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( not |.r.| <= 1 or r * M c= M )
assume A4: |.r.| <= 1 ; :: thesis: r * M c= M
reconsider r = r as Real ;
for x being Element of V st x in r * M holds
x in M

proof

let x be Element of V; :: thesis: ( x in r * M implies x in M )
assume x in r * M ; :: thesis: x in M
then consider u being Element of V such that
A5: x = u and
A6: u in r * M ;
u in { (r * w) where w is Element of V : w in M } by A6, CONVEX1:def 1;
then ex w1 being Element of V st
( u = r * w1 & w1 in M ) ;
hence x in M by A3, A4, A5; :: thesis: verum

end;

hence r * M c= M ; :: thesis: verum