:: deftheorem defines "/\" FILTER_0:def 8 :
for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "/\" D2 = { (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 ) } ;