:: deftheorem defines squared LATSTONE:def 12 :
for B being Boolean Lattice holds B squared = { [a,b] where a, b is Element of B : a [= b } ;