let V be non empty RLSStruct ; :: thesis: for F being convex-membered Subset-Family of holds meet F is convex
let F be convex-membered Subset-Family of ; :: thesis: meet F is convex
for M being Subset of st M in F holds
M is convex by Def3;
hence meet F is convex by CONVEX1:15; :: thesis: verum