---

Step * of Lemma es-closed-open-interval-nil

∀es:EO. ∀e:E.  ([e;e) = [] ∈ (E List))
BY
{ (Auto
   THEN (RWO "assert_of_null<" 0 THENA Auto)
   THEN Unfold `es-closed-open-interval` 0
   THEN (BLemma `null_filter` THENA Auto)
   THEN (BLemma `l_all_iff` THENA Auto)
   THEN RepUR ``so_apply`` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN GenListD (-2)
   THEN (FLemma `es-locl_transitivity2` [-1;-2] THENA Auto)
   THEN FLemma `es-locl_irreflexivity` [-1]
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.    ([e;e)  =  [])


By

(Auto
  THEN  (RWO  "assert\_of\_null<"  0  THENA  Auto)
  THEN  Unfold  `es-closed-open-interval`  0
  THEN  (BLemma  `null\_filter`  THENA  Auto)
  THEN  (BLemma  `l\_all\_iff`  THENA  Auto)
  THEN  RepUR  ``so\_apply``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  GenListD  (-2)
  THEN  (FLemma  `es-locl\_transitivity2`  [-1;-2]  THENA  Auto)
  THEN  FLemma  `es-locl\_irreflexivity`  [-1]
  THEN  Auto)

---

Home Index