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