thus ( M is circled implies for u being VECTOR of V
for r being Real st abs r <= 1 & u in M holds
r * u in M ) :: thesis: ( ( for u being VECTOR of V
for r being Real st abs 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 abs r <= 1 & u in M holds
r * u in M
let u be VECTOR of V; :: thesis: for r being Real st abs r <= 1 & u in M holds
r * u in M
let r be Real; :: thesis: ( abs r <= 1 & u in M implies r * u in M )
assume A2: abs r <= 1 ; :: thesis: ( not u in M or r * u in M )
assume u in M ; :: thesis: r * u in M
then A3: r * u in r * M by RLTOPSP1:1;
r * M c= M by A1, A2, RLTOPSP1:def 6;
hence r * u in M by A3; :: thesis: verum

end;

assume A4: for u being VECTOR of V
for r being Real st abs 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 abs r <= 1 or r * M c= M )
assume A5: abs r <= 1 ; :: thesis: r * M c= M
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
A6: ( x = u & u in r * M ) ;
u in { (r * w) where w is Element of V : w in M } by A6, CONVEX1:def 1;
then consider w1 being Element of V such that
A7: ( u = r * w1 & w1 in M ) ;
thus x in M by A4, A5, A6, A7; :: thesis: verum

end;

hence r * M c= M by SUBSET_1:7; :: thesis: verum