---

Step * 1 2 of Lemma pair-sq-axiom-wf


1. a : Top
2. b : Top
3. ∀x,y:Base.  ((<x, y> ~ Ax) ⇒ False)
⊢ <a, b> ~ Ax ∈ Type
BY
{ TACTIC:((PointwiseFunctionalityForEquality (-3) THENA Auto)
          THEN (PointwiseFunctionalityForEquality (-2) THENA Auto)
          ) }

1
1. a : Base
2. a1 : Base
3. a = a1 ∈ Top
4. b : Base
5. b1 : Base
6. b = b1 ∈ Top
7. ∀x,y:Base.  ((<x, y> ~ Ax) ⇒ False)
⊢ (<a, b> ~ Ax) = (<a1, b1> ~ Ax) ∈ Type

---

Latex:

---

Latex:

1.  a  :  Top
2.  b  :  Top
3.  \mforall{}x,y:Base.    ((<x,  y>  \msim{}  Ax)  {}\mRightarrow{}  False)
\mvdash{}  <a,  b>  \msim{}  Ax  \mmember{}  Type


By

---

Latex:
TACTIC:((PointwiseFunctionalityForEquality  (-3)  THENA  Auto)
                THEN  (PointwiseFunctionalityForEquality  (-2)  THENA  Auto)
                )

---

Home Index