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;
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;