let A be non empty set ; :: thesis: 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:] holds d c= new_bi_fun (d,q)

let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun (d,q)

let d be BiFunction of A,L; :: thesis: for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun (d,q)
let q be Element of [:A,A, the carrier of L, the carrier of L:]; :: thesis: d c= new_bi_fun (d,q)
set g = new_bi_fun (d,q);
A1: A c= new_set A by XBOOLE_1:7;
A2: for z being object st z in dom d holds
d . z = (new_bi_fun (d,q)) . z
proof
let z be object ; :: thesis: ( z in dom d implies d . z = (new_bi_fun (d,q)) . z )
assume A3: z in dom d ; :: thesis: d . z = (new_bi_fun (d,q)) . z
then consider x, y being object such that
A4: [x,y] = z by RELAT_1:def 1;
reconsider x9 = x, y9 = y as Element of A by ;
d . [x,y] = d . (x9,y9)
.= (new_bi_fun (d,q)) . (x9,y9) by Def10
.= (new_bi_fun (d,q)) . [x,y] ;
hence d . z = (new_bi_fun (d,q)) . z by A4; :: thesis: verum
end;
( dom d = [:A,A:] & dom (new_bi_fun (d,q)) = [:(),():] ) by FUNCT_2:def 1;
then dom d c= dom (new_bi_fun (d,q)) by ;
hence d c= new_bi_fun (d,q) by ; :: thesis: verum