theorem Th38: :: LATTICE4:38

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