---

Step * of Lemma eq-Game_wf

∀[G,H:Game].  (G ≡ H ∈ ℙ)
BY
{ (Auto THEN (Assert ⌜∀H:Game. ((G ≡ H ∈ ℙ) ∧ (H ≡ G ∈ ℙ))⌝⋅ THENM Auto) THEN Thin (-1)) }

1
1. G : Game
⊢ ∀H:Game. ((G ≡ H ∈ ℙ) ∧ (H ≡ G ∈ ℙ))

---

Latex:

---

Latex:
\mforall{}[G,H:Game].    (G  \mequiv{}  H  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  (Assert  \mkleeneopen{}\mforall{}H:Game.  ((G  \mequiv{}  H  \mmember{}  \mBbbP{})  \mwedge{}  (H  \mequiv{}  G  \mmember{}  \mBbbP{}))\mkleeneclose{}\mcdot{}  THENM  Auto)  THEN  Thin  (-1))

---

Home Index