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: ( abs r <= 1 implies r * (union F) c= union F )
assume A1: abs r <= 1 ; :: thesis: r * (union F) c= union F
let x be set ; :: 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 x' being Point of X such that
A2: x = r * x' and
A3: x' in union F ;
consider Y being set such that
A4: x' 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, Def6;
r * x' in r * Y by A4;
hence x in union F by A2, A5, A6, TARSKI:def 4; :: thesis: verum