defpred S₁[ 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₁[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 by A4;
A6: f is u.t.i.

proof

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 ;

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

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;

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

proof

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

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;

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

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

proof

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

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;

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;

end;

end;

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

end;

end;

end;

end;

end;

end;

f is symmetric

proof

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 ;

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 A13: x <> y ; :: thesis: f . (x,y) = f . (y,x)

hence f . (x,y) = y9 "\/" x9 by A4
.= f . (y,x) by A4, A13 ;
:: thesis: verum

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