---

Step * of Lemma fl-morph-join

∀[A,B:fset(ℕ)]. ∀[g:A ⟶ B]. ∀[x,y:Point(face_lattice(B))].  ((x ∨ y)<g> = (x)<g> ∨ (y)<g> ∈ Point(face_lattice(A)))
BY
{ ((UnivCD THENA Auto) THEN GenConclAtAddr [2;1] THEN Symmetry THEN RepeatFor 2 ((DVar `v' THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[A,B:fset(\mBbbN{})].  \mforall{}[g:A  {}\mrightarrow{}  B].  \mforall{}[x,y:Point(face\_lattice(B))].    ((x  \mvee{}  y)<g>  =  (x)<g>  \mvee{}  (y)<g>)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  GenConclAtAddr  [2;1]
  THEN  Symmetry
  THEN  RepeatFor  2  ((DVar  `v'  THEN  Auto)))

---

Home Index