:: deftheorem defines "\/" FILTER_2:def 11 :
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 ) } ;