let X be non empty RealLinearSpace; :: thesis: for A, B being circled Subset of X holds A + B is circled
let A, B be circled Subset of X; :: thesis: A + B is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( abs r <= 1 implies r * (A + B) c= A + B )
assume A1: abs r <= 1 ; :: thesis: r * (A + B) c= A + B
A2: A + B = { (u + v) where u, v is Point of X : ( u in A & v in B ) } by RUSUB_4:def 10;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (A + B) or x in A + B )
assume x in r * (A + B) ; :: thesis: x in A + B
then consider x' being Point of X such that
A3: x = r * x' and
A4: x' in A + B ;
consider u, v being Point of X such that
A5: x' = u + v and
A6: u in A and
A7: v in B by A2, A4;
A8: ( r * A c= A & r * B c= B ) by A1, Def6;
A9: ( r * u in r * A & r * v in r * B ) by A6, A7;
x = (r * u) + (r * v) by A3, A5, RLVECT_1:def 9;
hence x in A + B by A8, A9, Th3; :: thesis: verum