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;
A2: dom (alpha d) = the carrier of L by FUNCT_2:def 1;
consider E1 being Equivalence_Relation of A such that
A3: ( E1 = (alpha d) . a & ( for x, y being Element of A holds
( [x,y] in E1 iff d . x,y <= a ) ) ) by Def9;
consider E2 being Equivalence_Relation of A such that
A4: ( E2 = (alpha d) . b & ( for x, y being Element of A holds
( [x,y] in E2 iff d . x,y <= b ) ) ) by Def9;
consider E3 being Equivalence_Relation of A such that
A5: ( E3 = (alpha d) . (a "/\" b) & ( for x, y being Element of A holds
( [x,y] in E3 iff d . x,y <= a "/\" b ) ) ) by Def9;
A6: 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 [x,y] in E1 /\ E2 ; :: thesis: [x,y] in E3
then ( [x,y] in E1 & [x,y] in E2 ) by XBOOLE_0:def 4;
then ( d . x,y <= a & d . x,y <= b ) by A3, A4;
then d . x,y <= a "/\" b by YELLOW_0:23;
hence [x,y] in E3 by A5; :: thesis: verum

end;

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

end;

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

proof

let x, y be set ; :: thesis: ( [x,y] in E1 /\ E2 iff [x,y] in E3 )
A10: field E3 = A by EQREL_1:16;
(field E1) /\ (field E2) = A /\ (field E2) by EQREL_1:16
.= A /\ A by EQREL_1:16
.= A ;
then A11: field (E1 /\ E2) c= A by RELAT_1:34;

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

assume A12: [x,y] in E1 /\ E2 ; :: thesis: [x,y] in E3
then ( x in field (E1 /\ E2) & y in field (E1 /\ E2) ) by RELAT_1:30;
then reconsider x' = x, y' = y as Element of A by A11;
[x',y'] in E3 by A6, A12;
hence [x,y] in E3 ; :: thesis: verum

end;

assume A13: [x,y] in E3 ; :: thesis: [x,y] in E1 /\ E2
then reconsider x' = x, y' = y as Element of A by A10, RELAT_1:30;
[x',y'] in E1 /\ E2 by A6, A13;
hence [x,y] in E1 /\ E2 ; :: thesis: verum

end;

inf ((alpha d) .: {a,b}) = inf {((alpha d) . a),((alpha d) . b)} by A2, FUNCT_1:118
.= ((alpha d) . a) "/\" ((alpha d) . b) by YELLOW_0:40
.= E1 /\ E2 by A3, A4, Th8
.= (alpha d) . (a "/\" b) by A5, A9, RELAT_1:def 2
.= (alpha d) . (inf {a,b}) by YELLOW_0:40 ;
hence alpha d preserves_inf_of {a,b} by A1, WAYBEL_0:def 30; :: thesis: verum