let BL be Boolean Lattice; :: thesis: 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 `)
let b be Element of BL; :: thesis: for B being Element of Fin the carrier of BL holds FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
let B be Element of Fin the carrier of BL; :: thesis: FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" (b `)
thus FinMeet ((B \/ {.b.}),(comp BL)) = (FinMeet (B,(comp BL))) "/\" ((comp BL) . b) by Th20
.= (FinMeet (B,(comp BL))) "/\" (b `) by Def12 ; :: thesis: verum