---

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


1. a : Top
2. b : Top
⊢ <a, b> ~ Ax ∈ Type
BY
{ TACTIC:Assert ⌜∀x,y:Base.  ((<x, y> ~ Ax) ⇒ False)⌝⋅ }

1
.....assertion..... 
1. a : Top
2. b : Top
⊢ ∀x,y:Base.  ((<x, y> ~ Ax) ⇒ False)

2
1. a : Top
2. b : Top
3. ∀x,y:Base.  ((<x, y> ~ Ax) ⇒ False)
⊢ <a, b> ~ Ax ∈ Type

---

Latex:

---

Latex:

1.  a  :  Top
2.  b  :  Top
\mvdash{}  <a,  b>  \msim{}  Ax  \mmember{}  Type


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}\mforall{}x,y:Base.    ((<x,  y>  \msim{}  Ax)  {}\mRightarrow{}  False)\mkleeneclose{}\mcdot{}

---

Home Index