for L being Lattice
for u being Element of L
for A being non empty set
for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)