:: deftheorem Def4 defines new_bi_fun2 LATTICE8:def 4 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:]
for b₅ being BiFunction of (new_set2 A),L holds
( b₅ = new_bi_fun2 (d,q) iff ( ( for u, v being Element of A holds b₅ . (u,v) = d . (u,v) ) & b₅ . ({A},{A}) = Bottom L & b₅ . ({{A}},{{A}}) = Bottom L & b₅ . ({A},{{A}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b₅ . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & ( for u being Element of A holds
( b₅ . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b₅ . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b₅ . (u,{{A}}) = (d . (u,(q `2_4))) "\/" (q `3_4) & b₅ . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) ) );