theorem :: LATTICE4:40

for BL being Boolean Lattice
for b being Element of BL
for B being Element of Fin the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)