theorem :: LATTICE3:21

for L being Lattice
for p, q, r being Element of L holds
( p is_less_than {q,r} iff p [= q "/\" r )