:: deftheorem Def10 defines new_bi_fun LATTICE5:def 10 :
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_set A),L holds
( b₅ = new_bi_fun (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}}}) = Bottom L & b₅ . ({{A}},{{{A}}}) = q `3_4 & b<sub>5</sub> . ({{{A}}},{{A}}) = q `3_4 & b₅ . ({A},{{A}}) = q `4_4 & b<sub>5</sub> . ({{A}},{A}) = q `4_4 & b₅ . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b₅ . ({{{A}}},{A}) = (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 `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b<sub>5</sub> . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b₅ . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b₅ . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) );