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]
proof
let x, y be Element of L; :: thesis: ex z being Element of L st S1[x,y,z]
per cases ( x = y or x <> y ) ;
suppose A2: x = y ; :: thesis: ex z being Element of L st S1[x,y,z]
take Bottom L ; :: thesis: S1[x,y, Bottom L]
thus S1[x,y, Bottom L] by A2; :: thesis: verum
end;
suppose A3: x <> y ; :: thesis: ex z being Element of L st S1[x,y,z]
take x "\/" y ; :: thesis: S1[x,y,x "\/" y]
thus S1[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 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; :: 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