:: deftheorem Def15 defines BiFun LATTICE5:def 15 :
for A being non empty set
for L being lower-bounded LATTICE
for z being set st z is BiFunction of A,L holds
BiFun (z,A,L) = z;