theorem :: LATTICE2:42

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 ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinMeet (B,f) = u by SETWISEO:24;