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 } ;
set x9 = the Element of A;
consider z being set such that
A1: z = [ the Element of A, the Element of A,(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 Def11;
d . ( the Element of A, the Element of A) = Bottom L by Def6
.= (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:26; :: thesis: verum