let X be non empty RLSStruct ; :: thesis: for F being circled-membered Subset-Family of X holds union F is circled
let F be circled-membered Subset-Family of X; :: thesis: union F is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.r.| <= 1 implies r * (union F) c= union F )
assume A1: |.r.| <= 1 ; :: thesis: r * (union F) c= union F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (union F) or x in union F )
assume x in r * (union F) ; :: thesis: x in union F
then consider x9 being Point of X such that
A2: x = r * x9 and
A3: x9 in union F ;
consider Y being set such that
A4: x9 in Y and
A5: Y in F by A3, TARSKI:def 4;
reconsider Y = Y as Subset of X by A5;
Y is circled by A5, Def7;
then A6: r * Y c= Y by A1;
r * x9 in r * Y by A4;
hence x in union F by A2, A5, A6, TARSKI:def 4; :: thesis: verum