:: deftheorem defines meet-closed LATTICES:def 24 :
for L being non empty LattStr
for S being Subset of L holds
( S is meet-closed iff for p, q being Element of L st p in S & q in S holds
p "/\" q in S );