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 x' being Element of A;
consider z being set such that
A1: z = [x',x',(Bottom L),(Bottom L)] ;
d . x',x' = Bottom L by Def7
.= (Bottom L) "\/" (Bottom L) by YELLOW_5:1 ;
then A2: 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;
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;
hence DistEsti d <> {} by A2, CARD_1:46; :: thesis: verum