for S being non empty 1-sorted
for N being net of S
for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds
ex B being Subset of S,N st B c= meet F