let X be non empty RLSStruct ; :: thesis: for F being circled-membered Subset-Family of X holds meet F is circled
let F be circled-membered Subset-Family of X; :: thesis: meet F is circled
let r be Real; :: according to RLTOPSP1:def 6 :: thesis: ( |.r.| <= 1 implies r * (meet F) c= meet F )
assume A1: |.r.| <= 1 ; :: thesis: r * (meet F) c= meet F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (meet F) or x in meet F )
assume x in r * (meet F) ; :: thesis: x in meet F
then consider x9 being Point of X such that
A2: x = r * x9 and
A3: x9 in meet F ;

A4: now :: thesis: for Y being set st Y in F holds
x in Y

let Y be set ; :: thesis: ( Y in F implies x in Y )
assume A5: Y in F ; :: thesis: x in Y
then reconsider Y9 = Y as Subset of X ;
x9 in Y by A3, A5, SETFAM_1:def 1;
then A6: r * x9 in r * Y9 ;
Y9 is circled by A5, Def7;
then r * Y9 c= Y9 by A1;
hence x in Y by A2, A6; :: thesis: verum

end;

F <> {} by A3, SETFAM_1:def 1;
hence x in meet F by A4, SETFAM_1:def 1; :: thesis: verum