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