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: ( abs r <= 1 implies r * (Cl B) c= Cl B )
assume A1: abs 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

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

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

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

end;

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

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

end;

end;

end;

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

end;

suppose A5: 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:49;
hence r * (Cl B) c= Cl B by A5, Th53; :: thesis: verum

end;

end;