for L being RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
X is upper ) holds
meet F is upper Subset of L