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 by FUNCOP_1:13;
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 by Def6;
for x being Element of A holds f . x,x = Bottom L by A1;
then A3: f is zeroed by Def7;
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
A4: ( f . x,y = Bottom L & f . y,z = Bottom L ) by A1;
f . x,z <= Bottom L by A1;
hence (f . x,y) "\/" (f . y,z) >= f . x,z by A4, YELLOW_5:1; :: thesis: verum

end;

then f is u.t.i. by Def8;
hence ex b₁ being BiFunction of A,L st
( b₁ is symmetric & b₁ is zeroed & b₁ is u.t.i. ) by A2, A3; :: thesis: verum