theorem PseudoInSquared: :: LATSTONE:39

for B being Boolean Lattice
for L being Lattice
for x1, x2 being Element of B
for x being Element of L st L = B squared-latt & x = [x1,x2] holds
x * = [(x2 `),(x2 `)]