let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L holds DistEsti d <> {}
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L holds DistEsti d <> {}
let d be distance_function of A,L; :: thesis: DistEsti d <> {}
set X = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ;
consider x9 being Element of A;
consider z being set such that
A1: z = [x9,x9,(Bottom L),(Bottom L)] ;
A2: DistEsti d,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent by Def12;
d . x9,x9 = Bottom L by Def7
.= (Bottom L) "\/" (Bottom L) by YELLOW_5:1 ;
then z in { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } by A1;
hence DistEsti d <> {} by A2, CARD_1:46; :: thesis: verum