theorem :: LATTICE3:5

for X being set
for x being Element of (BooleLatt X) holds x ` = X \ x