defpred S1[ Element of L, Element of L, set ] means ( ( $1 = $2 implies $3 = Bottom L ) & ( $1 <> $2 implies $3 = $1 "\/" $2 ) );
set A = the carrier of L;
A1:
for x, y being Element of L ex z being Element of L st S1[x,y,z]
consider f being Function of [: the carrier of L, the carrier of L:], the carrier of L such that
A4:
for x, y being Element of L holds S1[x,y,f . (x,y)]
from BINOP_1:sch 3(A1);
reconsider f = f as BiFunction of the carrier of L,L ;
A5:
f is zeroed
by A4;
A6:
f is u.t.i.
proof
let x,
y,
z be
Element of the
carrier of
L;
LATTICE5:def 7 (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
L ;
per cases
( x = z or x <> z )
;
suppose A8:
x <> z
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)thus
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
verumproof
per cases
( x = y or x <> y )
;
suppose A9:
x = y
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)
x9 "\/" z9 >= x9 "\/" z9
by ORDERS_2:1;
then
f . (
x,
z)
>= x9 "\/" z9
by A4, A8;
then
(Bottom L) "\/" (f . (x,z)) >= x9 "\/" z9
by WAYBEL_1:3;
then
(f . (x,y)) "\/" (f . (y,z)) >= x9 "\/" z9
by A4, A9;
hence
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A4, A8;
verum end; end;
end; end; end;
end;
f is symmetric
then reconsider f = f as distance_function of the carrier of L,L by A5, A6;
take
f
; for x, y being Element of L holds
( ( x <> y implies f . (x,y) = x "\/" y ) & ( x = y implies f . (x,y) = Bottom L ) )
thus
for x, y being Element of L holds
( ( x <> y implies f . (x,y) = x "\/" y ) & ( x = y implies f . (x,y) = Bottom L ) )
by A4; verum