defpred S_{1}[ 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 S_{1}[x,y,z]

A4: for x, y being Element of L holds S_{1}[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.

take f ; :: thesis: 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; :: thesis: verum

set A = the carrier of L;

A1: for x, y being Element of L ex z being Element of L st S

proof

consider f being Function of [: the carrier of L, the carrier of L:], the carrier of L such that
let x, y be Element of L; :: thesis: ex z being Element of L st S_{1}[x,y,z]

end;A4: for x, y being Element of L holds S

reconsider f = f as BiFunction of the carrier of L,L ;

A5: f is zeroed by A4;

A6: f is u.t.i.

proof

f is symmetric
let x, y, z be Element of the carrier of L; :: according to LATTICE5:def 7 :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

reconsider x9 = x, y9 = y, z9 = z as Element of L ;

end;reconsider x9 = x, y9 = y, z9 = z as Element of L ;

per cases
( x = z or x <> z )
;

end;

suppose A7:
x = z
; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

(f . (x,y)) "\/" (f . (y,z)) >= Bottom L
by YELLOW_0:44;

hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A4, A7; :: thesis: verum

end;hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A4, A7; :: thesis: verum

suppose A8:
x <> z
; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

thus
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)
:: thesis: verum

end;proof
end;

per cases
( x = y or x <> y )
;

end;

suppose A9:
x = y
; :: thesis: (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; :: thesis: verum

end;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; :: thesis: verum

suppose A10:
x <> y
; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

(x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9

hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A4, A8; :: thesis: verum

end;proof
end;

then
(f . (x,y)) "\/" (f . (y,z)) >= x9 "\/" z9
by A4, A10;per cases
( y = z or y <> z )
;

end;

suppose A11:
y = z
; :: thesis: (x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9

x9 "\/" y9 >= x9 "\/" y9
by ORDERS_2:1;

then (Bottom L) "\/" (x9 "\/" y9) >= x9 "\/" z9 by A11, WAYBEL_1:3;

hence (x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9 by A4, A11; :: thesis: verum

end;then (Bottom L) "\/" (x9 "\/" y9) >= x9 "\/" z9 by A11, WAYBEL_1:3;

hence (x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9 by A4, A11; :: thesis: verum

suppose A12:
y <> z
; :: thesis: (x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9

(x9 "\/" z9) "\/" y9 =
(x9 "\/" z9) "\/" (y9 "\/" y9)
by YELLOW_5:1

.= x9 "\/" (z9 "\/" (y9 "\/" y9)) by LATTICE3:14

.= x9 "\/" (y9 "\/" (y9 "\/" z9)) by LATTICE3:14

.= (x9 "\/" y9) "\/" (y9 "\/" z9) by LATTICE3:14 ;

then (x9 "\/" y9) "\/" (y9 "\/" z9) >= x9 "\/" z9 by YELLOW_0:22;

hence (x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9 by A4, A12; :: thesis: verum

end;.= x9 "\/" (z9 "\/" (y9 "\/" y9)) by LATTICE3:14

.= x9 "\/" (y9 "\/" (y9 "\/" z9)) by LATTICE3:14

.= (x9 "\/" y9) "\/" (y9 "\/" z9) by LATTICE3:14 ;

then (x9 "\/" y9) "\/" (y9 "\/" z9) >= x9 "\/" z9 by YELLOW_0:22;

hence (x9 "\/" y9) "\/" (f . (y,z)) >= x9 "\/" z9 by A4, A12; :: thesis: verum

hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A4, A8; :: thesis: verum

proof

then reconsider f = f as distance_function of the carrier of L,L by A5, A6;
let x, y be Element of the carrier of L; :: according to LATTICE5:def 5 :: thesis: f . (x,y) = f . (y,x)

reconsider x9 = x, y9 = y as Element of L ;

end;reconsider x9 = x, y9 = y as Element of L ;

take f ; :: thesis: 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; :: thesis: verum