---

Step * 2 2 1 1 of Lemma fl-meet-0-1


1. T : Type
2. eq : EqDecider(T)
⊢ ∀a,b:Point(face-lattice(T;eq)).
    ((/\({} ⋃ {a} ⋃ {b}) = 0 ∈ Point(face-lattice(T;eq))) ⇒ (a ∧ b = 0 ∈ Point(face-lattice(T;eq))))
BY
{ GenConcl ⌜deq-fset(deq-fset(union-deq(T;T;eq;eq))) = ee ∈ EqDecider(Point(face-lattice(T;eq)))⌝⋅ }

1
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
⊢ deq-fset(deq-fset(union-deq(T;T;eq;eq))) ∈ EqDecider(Point(face-lattice(T;eq)))

2
1. T : Type
2. eq : EqDecider(T)
3. ee : EqDecider(Point(face-lattice(T;eq)))
4. deq-fset(deq-fset(union-deq(T;T;eq;eq))) = ee ∈ EqDecider(Point(face-lattice(T;eq)))
⊢ ∀a,b:Point(face-lattice(T;eq)).
    ((/\({} ⋃ {a} ⋃ {b}) = 0 ∈ Point(face-lattice(T;eq))) ⇒ (a ∧ b = 0 ∈ Point(face-lattice(T;eq))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  \mforall{}a,b:Point(face-lattice(T;eq)).    ((/\mbackslash{}(\{\}  \mcup{}  \{a\}  \mcup{}  \{b\})  =  0)  {}\mRightarrow{}  (a  \mwedge{}  b  =  0))


By

---

Latex:
GenConcl  \mkleeneopen{}deq-fset(deq-fset(union-deq(T;T;eq;eq)))  =  ee\mkleeneclose{}\mcdot{}

---

Home Index