reconsider f = [:A,A:] --> (Bottom L) as Function of [:A,A:], the carrier of L ;
A1: for x, y being Element of A holds f . [x,y] = Bottom L ;
reconsider f = f as BiFunction of A,L ;
for x, y being Element of A holds f . (x,y) = f . (y,x)

proof

let x, y be Element of A; :: thesis: f . (x,y) = f . (y,x)
thus f . (x,y) = Bottom L by A1
.= f . (y,x) by A1 ; :: thesis: verum

end;

then A2: f is symmetric ;
for x, y, z being Element of A holds (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

proof

let x, y, z be Element of A; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)
A3: f . (x,z) <= Bottom L by A1;
( f . (x,y) = Bottom L & f . (y,z) = Bottom L ) by A1;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A3, YELLOW_5:1; :: thesis: verum

end;

then A4: f is u.t.i. ;
for x being Element of A holds f . (x,x) = Bottom L by A1;
then f is zeroed ;
hence ex b₁ being BiFunction of A,L st
( b₁ is symmetric & b₁ is zeroed & b₁ is u.t.i. ) by A2, A4; :: thesis: verum