let BL be Boolean Lattice; :: thesis: for b being Element of BL
for B being Finite_Subset of the carrier of BL holds FinJoin (B \/ {.b.}),(comp BL) = (FinJoin B,(comp BL)) "\/" (b ` )
let b be Element of BL; :: thesis: for B being Finite_Subset of the carrier of BL holds FinJoin (B \/ {.b.}),(comp BL) = (FinJoin B,(comp BL)) "\/" (b ` )
let B be Finite_Subset of the carrier of BL; :: thesis: FinJoin (B \/ {.b.}),(comp BL) = (FinJoin B,(comp BL)) "\/" (b ` )
thus FinJoin (B \/ {.b.}),(comp BL) = (FinJoin B,(comp BL)) "\/" ((comp BL) . b) by Th20
.= (FinJoin B,(comp BL)) "\/" (b ` ) by Def17 ; :: thesis: verum