:: deftheorem Def12 defines comp LATTICE4:def 13 :
for BL being Boolean Lattice
for b₂ being Function of the carrier of BL, the carrier of BL holds
( b₂ = comp BL iff for a being Element of BL holds b₂ . a = a ` );