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:11
.= (v0 "\/" v1) "/\" (v0 "\/" v2) ;
hence v0 "\/" (v1 "/\" v2) = (v0 "\/" v1) "/\" (v0 "\/" v2) ; :: thesis: verum