set A = the carrier of L;
defpred S₁[ Element of L, Element of L, set ] means ( ( $1 = $2 implies $3 = Bottom L ) & ( $1 <> $2 implies $3 = $1 "\/" $2 ) );
A1: for x, y being Element of L ex z being Element of L st S₁[x,y,z]

proof

let x, y be Element of L; :: thesis: ex z being Element of L st S₁[x,y,z]

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

suppose A2: x = y ; :: thesis: ex z being Element of L st S₁[x,y,z]

take Bottom L ; :: thesis: S₁[x,y, Bottom L]
thus S₁[x,y, Bottom L] by A2; :: thesis: verum

end;

suppose A3: x <> y ; :: thesis: ex z being Element of L st S₁[x,y,z]

take x "\/" y ; :: thesis: S₁[x,y,x "\/" y]
thus S₁[x,y,x "\/" y] by A3; :: thesis: verum

end;

end;

end;

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 S₁[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

proof

let x be Element of the carrier of L; :: according to LATTICE5:def 7 :: thesis: f . x,x = Bottom L
thus f . x,x = Bottom L by A4; :: thesis: verum

end;

A6: f is symmetric

proof

let x, y be Element of the carrier of L; :: according to LATTICE5:def 6 :: thesis: f . x,y = f . y,x
reconsider x' = x, y' = y as Element of L ;

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

suppose x = y ; :: thesis: f . x,y = f . y,x

hence f . x,y = f . y,x ; :: thesis: verum

end;

suppose A7: x <> y ; :: thesis: f . x,y = f . y,x

hence f . x,y = y' "\/" x' by A4
.= f . y,x by A4, A7 ;
:: thesis: verum

end;

end;

end;

f is u.t.i.

proof

let x, y, z be Element of the carrier of L; :: according to LATTICE5:def 8 :: thesis: (f . x,y) "\/" (f . y,z) >= f . x,z
reconsider x' = x, y' = y, z' = z as Element of L ;

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

suppose A8: 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, A8; :: thesis: verum

end;

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

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

proof

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

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

x' "\/" z' >= x' "\/" z' by ORDERS_2:24;
then f . x,z >= x' "\/" z' by A4, A9;
then (Bottom L) "\/" (f . x,z) >= x' "\/" z' by WAYBEL_1:4;
then (f . x,y) "\/" (f . y,z) >= x' "\/" z' by A4, A10;
hence (f . x,y) "\/" (f . y,z) >= f . x,z by A4, A9; :: thesis: verum

end;

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

(x' "\/" y') "\/" (f . y,z) >= x' "\/" z'

proof

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

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

x' "\/" y' >= x' "\/" y' by ORDERS_2:24;
then (Bottom L) "\/" (x' "\/" y') >= x' "\/" z' by A12, WAYBEL_1:4;
hence (x' "\/" y') "\/" (f . y,z) >= x' "\/" z' by A4, A12; :: thesis: verum

end;

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

(x' "\/" z') "\/" y' = (x' "\/" z') "\/" (y' "\/" y') by YELLOW_5:1
.= x' "\/" (z' "\/" (y' "\/" y')) by LATTICE3:14
.= x' "\/" (y' "\/" (y' "\/" z')) by LATTICE3:14
.= (x' "\/" y') "\/" (y' "\/" z') by LATTICE3:14 ;
then (x' "\/" y') "\/" (y' "\/" z') >= x' "\/" z' by YELLOW_0:22;
hence (x' "\/" y') "\/" (f . y,z) >= x' "\/" z' by A4, A13; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

end;

end;

end;

then reconsider f = f as distance_function of the carrier of L,L by A5, A6;
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