:: deftheorem defines *' LATTICE6:def 6 :
for L being complete Lattice
for a being Element of L holds a *' = "/\" ( { d where d is Element of L : ( a [= d & d <> a ) } ,L);