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
A1: A - B = { (u - v) where u, v is VECTOR of V : ( u in A & v in B ) } by RUSUB_5:def 2;
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( not |.r.| <= 1 or r * (A - B) c= A - B )
assume |.r.| <= 1 ; :: thesis: r * (A - B) c= A - B
then A2: ( r * A c= A & r * B c= B ) by RLTOPSP1:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (A - B) or x in A - B )
assume A3: x in r * (A - B) ; :: thesis: x in A - B
r * (A - B) = { (r * v) where v is VECTOR of V : v in A - B } by CONVEX1:def 1;
then consider x9 being VECTOR of V such that
A4: x = r * x9 and
A5: x9 in A - B by A3;
consider u, v being VECTOR of V such that
A6: x9 = u - v and
A7: ( u in A & v in B ) by A1, A5;
reconsider r = r as Real ;
A8: ( r * u in r * A & r * v in r * B ) by A7, RLTOPSP1:1;
x = (r * u) - (r * v) by A4, A6, RLVECT_1:34;
hence x in A - B by A2, A8, Lm1; :: thesis: verum