let A be non empty set ; for L being lower-bounded LATTICE
for d being distance_function of A,L holds DistEsti d <> {}
let L be lower-bounded LATTICE; for d being distance_function of A,L holds DistEsti d <> {}
let d be distance_function of A,L; 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; verum