:: deftheorem defines "/\" LATTICE3:def 22 :
for L being non empty LattStr
for X being set holds "/\" (X,L) = "\/" ( { p where p is Element of L : p is_less_than X } ,L);