for L being non trivial B_Lattice
for D being non empty Subset of L st Bottom L in <.D.) holds
ex B being non empty Element of Fin the carrier of L st
( B c= D & FinMeet B = Bottom L )