---

Step * of Lemma pairwise-singleton

∀P,v:Top.  ((∀x,y∈[v].  P[x;y]) ⇐⇒ True)
BY
{ ((UnivCD THENA Auto) THEN Unfold `pairwise` 0 THEN Reduce 0 THEN D 0 THEN D 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}P,v:Top.    ((\mforall{}x,y\mmember{}[v].    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  True)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `pairwise`  0  THEN  Reduce  0  THEN  D  0  THEN  D  0  THEN  Auto')

---

Home Index