---

Step * 2 1 1 of Lemma fl-point


1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. ∀a:fset(T + T). (a ∈ x ⇒ (∀z:T. (¬(inl z ∈ a ∧ inr z  ∈ a))))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
7. a : fset(T + T)
8. a ∈ x
9. z : T
10. inr z  ∈ a
11. c : fset(T + T)
12. c = {inl z,inr z } ∈ fset(T + T)
13. {inl z,inr z } ⊆ a
⊢ inl z ∈ a
BY
{ (BackThruHyp' (-1) THEN EAuto 1) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  fset(fset(T  +  T))
4.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
5.  \mforall{}a:fset(T  +  T).  (a  \mmember{}  x  {}\mRightarrow{}  (\mforall{}z:T.  (\mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a))))
6.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
7.  a  :  fset(T  +  T)
8.  a  \mmember{}  x
9.  z  :  T
10.  inr  z    \mmember{}  a
11.  c  :  fset(T  +  T)
12.  c  =  \{inl  z,inr  z  \}
13.  \{inl  z,inr  z  \}  \msubseteq{}  a
\mvdash{}  inl  z  \mmember{}  a


By

---

Latex:
(BackThruHyp'  (-1)  THEN  EAuto  1)

---

Home Index