:: deftheorem defines squared-latt LATSTONE:def 13 :
for B being Boolean Lattice holds B squared-latt = latt ([:B,B:],(B squared));