theorem Th18: :: LATTICE5:18

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds
new_bi_fun (d,q) is u.t.i.