:: deftheorem defines SetImp LATTICE4:def 12 :
for BL being Boolean Lattice
for A being non empty Subset of BL holds SetImp A = { (a => b) where a, b is Element of BL : ( a in A & b in A ) } ;