let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L holds alpha d is meet-preserving
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L holds alpha d is meet-preserving
let d be distance_function of A,L; :: thesis: alpha d is meet-preserving
let a, b be Element of L; :: according to WAYBEL_0:def 34 :: thesis: alpha d preserves_inf_of {a,b}
set f = alpha d;
A1: ex_inf_of (alpha d) .: {a,b}, EqRelLATT A by YELLOW_0:17;
consider E3 being Equivalence_Relation of A such that
A2: E3 = (alpha d) . (a "/\" b) and
A3: for x, y being Element of A holds
( [x,y] in E3 iff d . (x,y) <= a "/\" b ) by Def8;
consider E2 being Equivalence_Relation of A such that
A4: E2 = (alpha d) . b and
A5: for x, y being Element of A holds
( [x,y] in E2 iff d . (x,y) <= b ) by Def8;
consider E1 being Equivalence_Relation of A such that
A6: E1 = (alpha d) . a and
A7: for x, y being Element of A holds
( [x,y] in E1 iff d . (x,y) <= a ) by Def8;
A8: for x, y being Element of A holds
( [x,y] in E1 /\ E2 iff [x,y] in E3 )

proof

let x, y be Element of A; :: thesis: ( [x,y] in E1 /\ E2 iff [x,y] in E3 )

hereby :: thesis: ( [x,y] in E3 implies [x,y] in E1 /\ E2 )

assume A9: [x,y] in E1 /\ E2 ; :: thesis: [x,y] in E3
then [x,y] in E2 by XBOOLE_0:def 4;
then A10: d . (x,y) <= b by A5;
[x,y] in E1 by A9, XBOOLE_0:def 4;
then d . (x,y) <= a by A7;
then d . (x,y) <= a "/\" b by A10, YELLOW_0:23;
hence [x,y] in E3 by A3; :: thesis: verum

end;

assume [x,y] in E3 ; :: thesis: [x,y] in E1 /\ E2
then A11: d . (x,y) <= a "/\" b by A3;
a "/\" b <= b by YELLOW_0:23;
then d . (x,y) <= b by A11, ORDERS_2:3;
then A12: [x,y] in E2 by A5;
a "/\" b <= a by YELLOW_0:23;
then d . (x,y) <= a by A11, ORDERS_2:3;
then [x,y] in E1 by A7;
hence [x,y] in E1 /\ E2 by A12, XBOOLE_0:def 4; :: thesis: verum

end;

A13: for x, y being object holds
( [x,y] in E1 /\ E2 iff [x,y] in E3 )

proof

let x, y be object ; :: thesis: ( [x,y] in E1 /\ E2 iff [x,y] in E3 )
(field E1) /\ (field E2) = A /\ (field E2) by EQREL_1:9
.= A /\ A by EQREL_1:9
.= A ;
then A14: field (E1 /\ E2) c= A by RELAT_1:19;

hereby :: thesis: ( [x,y] in E3 implies [x,y] in E1 /\ E2 )

assume A15: [x,y] in E1 /\ E2 ; :: thesis: [x,y] in E3
then ( x in field (E1 /\ E2) & y in field (E1 /\ E2) ) by RELAT_1:15;
then reconsider x9 = x, y9 = y as Element of A by A14;
[x9,y9] in E3 by A8, A15;
hence [x,y] in E3 ; :: thesis: verum

end;

assume A16: [x,y] in E3 ; :: thesis: [x,y] in E1 /\ E2
field E3 = A by EQREL_1:9;
then reconsider x9 = x, y9 = y as Element of A by A16, RELAT_1:15;
[x9,y9] in E1 /\ E2 by A8, A16;
hence [x,y] in E1 /\ E2 ; :: thesis: verum

end;

dom (alpha d) = the carrier of L by FUNCT_2:def 1;
then inf ((alpha d) .: {a,b}) = inf {((alpha d) . a),((alpha d) . b)} by FUNCT_1:60
.= ((alpha d) . a) "/\" ((alpha d) . b) by YELLOW_0:40
.= E1 /\ E2 by A6, A4, Th8
.= (alpha d) . (a "/\" b) by A2, A13, RELAT_1:def 2
.= (alpha d) . (inf {a,b}) by YELLOW_0:40 ;
hence alpha d preserves_inf_of {a,b} by A1; :: thesis: verum