for BL being Boolean Lattice
for AF being non empty ClosedSubset of BL st Bottom BL in AF & Top BL in AF holds
for B being Element of Fin the carrier of BL st B c= SetImp AF holds
ex B0 being Element of Fin the carrier of BL st
( B0 c= SetImp AF & FinJoin (B,(comp BL)) = FinMeet B0 )