:: deftheorem defines <(1) LATTICE7:def 4 :
for L being LATTICE
for x, y being Element of L holds
( x <(1) y iff ( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) ) );