median_overlap[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY

BEGIN
  
  IMPORTING 
    reduce_properties[N, T, <=]

  e1, e2: VAR non_empty_finite_set[below(N)]
  v1, v2: VAR vec %[below(N) -> T]

  k: VAR below(N)

  median_overlap: LEMMA 
      card(union(e1, e2)) - card(intersection(e1, e2)) <= 1
    IMPLIES
      EXISTS k: 
        e1(k) AND 
        e2(k) AND 
        min(reduce(mid)(v1, e1)) <= v1(k) AND 
        v2(k) <= max(reduce(mid)(v2, e2))

END median_overlap