---

Step * of Lemma sq_stable_iff_uimplies

∀[P:ℙ]. (SqStable(P) ⇐⇒ P supposing P)
BY
{ Auto }

1
1. [P] : ℙ
2. SqStable(P)@i
3. [%1] : P
⊢ P

2
1. [P] : ℙ
2. P supposing P@i
⊢ SqStable(P)

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  (SqStable(P)  \mLeftarrow{}{}\mRightarrow{}  P  supposing  P)


By

---

Latex:
Auto

---

Home Index