theorem :: LATTICE4:39

for BL being Boolean Lattice
for B being Element of Fin the carrier of BL holds (FinJoin B) ` = FinMeet (B,(comp BL))