let L be B_Lattice; :: thesis: for a, b being Element of L holds (a "\/" b) ` = (a `) "/\" (b `)
let a, b be Element of L; :: thesis: (a "\/" b) ` = (a `) "/\" (b `)
thus (a "\/" b) ` = (((a `) `) "\/" ((b `) `)) `
.= (((a `) "/\" (b `)) `) ` by Th21
.= (a `) "/\" (b `) ; :: thesis: verum