for B being Boolean Lattice
for v0, v1 being Element of (BA2TBAA B)
for a, b being Element of B st a = v0 & b = v1 holds
v0 "\/" v1 = a "\/" b ;