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)
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;
(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;
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 b1 being BiFunction of A,L st
( b1 is symmetric & b1 is zeroed & b1 is u.t.i. )
by A2, A4; verum