let X be LinearTopSpace; :: thesis: for B being circled Subset of X holds Cl B is circled
let B be circled Subset of X; :: thesis: Cl B is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.r.| <= 1 implies r * (Cl B) c= Cl B )
assume A1: |.r.| <= 1 ; :: thesis: r * (Cl B) c= Cl B

per cases ( r = 0 or r <> 0 ) ;

suppose A2: r = 0 ; :: thesis: r * (Cl B) c= Cl B

now :: thesis: r * (Cl B) c= Cl B

per cases ( B = {} X or B <> {} X ) ;

suppose B = {} X ; :: thesis: r * (Cl B) c= Cl B

then Cl B = {} X by PRE_TOPC:22;
hence r * (Cl B) c= Cl B by CONVEX1:33; :: thesis: verum

end;

suppose A3: B <> {} X ; :: thesis: r * (Cl B) c= Cl B

A4: B c= Cl B by PRE_TOPC:18;
A5: 0. X in B by A3, Th27;
then r * (Cl B) = {(0. X)} by A2, A4, CONVEX1:34;
hence r * (Cl B) c= Cl B by A5, A4, ZFMISC_1:31; :: thesis: verum

end;

end;

end;

hence r * (Cl B) c= Cl B ; :: thesis: verum

end;

suppose A6: r <> 0 ; :: thesis: r * (Cl B) c= Cl B

r * B c= B by A1, Def6;
then Cl (r * B) c= Cl B by PRE_TOPC:19;
hence r * (Cl B) c= Cl B by A6, Th52; :: thesis: verum

end;

end;