%
% Purpose : Provide overlap results for tau = |E| - floor(N'/2) - 1
%
weber_overlap[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY 

  BEGIN

  IMPORTING
   reduce_properties[N, T, <=]

  src_set: VAR finite_set[below(N)]
  e, e1, e2 : var non_empty_finite_set[below(N)]
  v1, v2  : var [below(N) -> T]
  k: var below(N)

  tau(src_set): tau_type = weber(card(src_set))

  weber_overlap: LEMMA
      subset?(e1, src_set) AND
      subset?(e2, src_set) AND
      intersection_majority?(e1, e2, src_set)
    IMPLIES
      EXISTS k:
        src_set(k) AND
        e1(k) AND
        e2(k) AND
        min(reduce(tau(src_set))(v1, e1)) <= v1(k) AND
        v2(k) <= max(reduce(tau(src_set))(v2, e2))

  END weber_overlap