for BL being Boolean Lattice
for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
{ (FinMeet B) where B is Element of Fin the carrier of BL : B c= SetImp AF } = field_by AF