let V be RealLinearSpace; :: thesis: for A, B being circled Subset of V holds A - B is circled
let A, B be circled Subset of V; :: thesis: A - B is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( not abs r <= 1 or r * (A - B) c= A - B )
assume A1: abs r <= 1 ; :: thesis: r * (A - B) c= A - B
A2: r * (A - B) = { (r * v) where v is VECTOR of V : v in A - B } by CONVEX1:def 1;
A3: A - B = { (u - v) where u, v is VECTOR of V : ( u in A & v in B ) } by RUSUB_5:def 2;
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 VECTOR of V such that
A4: x = r * x' and
A5: x' in A - B by A2;
consider u, v being VECTOR of V such that
A6: x' = u - v and
A7: u in A and
A8: v in B by A3, A5;
A9: ( r * A c= A & r * B c= B ) by A1, RLTOPSP1:def 6;
A10: ( r * u in r * A & r * v in r * B ) by A7, A8, RLTOPSP1:1;
x = (r * u) - (r * v) by A4, A6, RLVECT_1:48;
hence x in A - B by A9, A10, Lm1; :: thesis: verum