let X be LinearTopSpace; :: thesis: for B being circled Subset of X st 0. X in Int B holds
Int B is circled
let B be circled Subset of X; :: thesis: ( 0. X in Int B implies Int B is circled )
assume A1: 0. X in Int B ; :: thesis: Int B is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.r.| <= 1 implies r * (Int B) c= Int B )
assume |.r.| <= 1 ; :: thesis: r * (Int B) c= Int B
then r * B c= B by Def6;
then A2: Int (r * B) c= Int B by TOPS_1:19;

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

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

then r * (Int B) = {(0. X)} by A1, CONVEX1:34;
hence r * (Int B) c= Int B by A1, ZFMISC_1:31; :: thesis: verum

end;

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

hence r * (Int B) c= Int B by A2, Th51; :: thesis: verum

end;

end;