theorem TBAComplA: :: LATTBA_1:13

for B being Boolean Lattice
for x being Element of B
for xx being Element of (BA2TBAA B) st xx = x holds
x ` = xx `