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: ( abs r <= 1 implies r * (meet F) c= meet F )
assume A1: abs r <= 1 ; :: thesis: r * (meet F) c= meet F
let x be set ; :: 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 x' being Point of X such that
A2: x = r * x' and
A3: x' in meet F ;
A4: F <> {} by A3, SETFAM_1:def 1;

now

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

end;

hence x in meet F by A4, SETFAM_1:def 1; :: thesis: verum