let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L holds succ {} c= DistEsti d
let d be distance_function of A,L; :: thesis: succ {} c= DistEsti d
( succ {} c= DistEsti d or DistEsti d in succ {} ) by ORDINAL1:16;
then ( succ {} c= DistEsti d or DistEsti d c= {} ) by ORDINAL1:22;
hence succ {} c= DistEsti d by LATTICE5:20, XBOOLE_1:3; :: thesis: verum