---

Step * of Lemma is-above-singleton-subtype

∀[A:Type]. ∀[a:A]. ∀[B:Type].  ∀[z:Base]. (is-above(A;a;z) ⇒ is-above(B;a;z)) supposing {x:A| x = a ∈ A}  ⊆r B
BY
{ (Auto THEN (Assert ⌜is-above({x:A| x = a ∈ A} ;a;z)⌝⋅ THENM (FLemma `is-above-subtype` [-1;4] THEN Auto))) }

1
.....assertion..... 
1. [A] : Type
2. [a] : A
3. [B] : Type
4. {x:A| x = a ∈ A}  ⊆r B
5. [z] : Base
6. is-above(A;a;z)
⊢ is-above({x:A| x = a ∈ A} ;a;z)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[a:A].  \mforall{}[B:Type].
    \mforall{}[z:Base].  (is-above(A;a;z)  {}\mRightarrow{}  is-above(B;a;z))  supposing  \{x:A|  x  =  a\}    \msubseteq{}r  B


By

---

Latex:
(Auto  THEN  (Assert  \mkleeneopen{}is-above(\{x:A|  x  =  a\}  ;a;z)\mkleeneclose{}\mcdot{}  THENM  (FLemma  `is-above-subtype`  [-1;4]  THEN  Auto)\000C))

---

Home Index