let B be Boolean Lattice; :: thesis: for v0, v2, v1 being Element of (BA2TBAA B) holds v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)
let v0, v2, v1 be Element of (BA2TBAA B); :: thesis: v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2)
reconsider cc = v2, aa = v0, bb = v1 as Element of B ;
v0 "/\" (v1 "\/" v2) = aa "/\" (bb "\/" cc)
.= (aa "/\" bb) "\/" (aa "/\" cc) by LATTICES:def 11
.= (v0 "/\" v1) "\/" (v0 "/\" v2) ;
hence v0 "/\" (v1 "\/" v2) = (v0 "/\" v1) "\/" (v0 "/\" v2) ; :: thesis: verum