---

Step * of Lemma not-not-inner-pasch

No Annotations
∀g:OrientedPlane. ∀a,b,c:Point. ∀p:{p:Point| B(apc)} . ∀q:{q:Point| B(bqc)} .  (¬¬(∃x:Point. (B(pxb) ∧ B(qxa))))
BY
{ (Auto
   THEN ((gSeparatedCases ⌜a⌝ ⌜p⌝⋅ THENA Auto)
         THENL [((gSeparatedCases ⌜b⌝ ⌜q⌝⋅ THENA Auto)
                 THENL [(DSetVars THENA Auto); ((RemoveDoubleNegation THENA Auto) THEN D 0 With ⌜q⌝  THEN Auto)]
               )
               ; ((RemoveDoubleNegation THENA Auto) THEN D 0 With ⌜p⌝  THEN Auto)]
   )
   THEN ((gSeparatedCases ⌜p⌝ ⌜c⌝⋅ THENA Auto)
         THENL [((gSeparatedCases ⌜q⌝ ⌜c⌝⋅ THENA Auto)
                 THENL [(StableCases ⌜c # ab⌝⋅ THENA Auto)
                       ; ((RemoveDoubleNegation THENA Auto) THEN D 0 With ⌜p⌝  THEN Auto)]
               )
               ; ((RemoveDoubleNegation THENA Auto) THEN D 0 With ⌜q⌝  THEN Auto)]
   )) }

1
1. g : OrientedPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. B(apc)
7. q : Point
8. B(bqc)
9. a # p
10. b # q
11. p # c
12. q # c
13. c # ab
⊢ ¬¬(∃x:Point. (B(pxb) ∧ B(qxa)))

2
1. g : OrientedPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. B(apc)
7. q : Point
8. B(bqc)
9. a # p
10. b # q
11. p # c
12. q # c
13. ¬c # ab
⊢ ¬¬(∃x:Point. (B(pxb) ∧ B(qxa)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:OrientedPlane.  \mforall{}a,b,c:Point.  \mforall{}p:\{p:Point|  B(apc)\}  .  \mforall{}q:\{q:Point|  B(bqc)\}  .
    (\mneg{}\mneg{}(\mexists{}x:Point.  (B(pxb)  \mwedge{}  B(qxa))))


By

---

Latex:
(Auto
  THEN  ((gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}p\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((gSeparatedCases  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THENL  [(DSetVars  THENA  Auto)
                                          ;  ((RemoveDoubleNegation  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}q\mkleeneclose{}    THEN  Auto)]
                          )
                          ;  ((RemoveDoubleNegation  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}p\mkleeneclose{}    THEN  Auto)]
  )
  THEN  ((gSeparatedCases  \mkleeneopen{}p\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [((gSeparatedCases  \mkleeneopen{}q\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THENL  [(StableCases  \mkleeneopen{}c  \#  ab\mkleeneclose{}\mcdot{}  THENA  Auto)
                                          ;  ((RemoveDoubleNegation  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}p\mkleeneclose{}    THEN  Auto)]
                          )
                          ;  ((RemoveDoubleNegation  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}q\mkleeneclose{}    THEN  Auto)]
  ))

---

Home Index